Syntax definition cei

Description: Extend class notation with Hilbert space eigenvector function.

	Ref	Expression
Assertion	cei	$$class\mathrm{eigvec}$$