Syntax Definition comu 3102

Description: Extend the definition of a class to include the ordinal multiplication operation.

Assertion

Ref	Expression
comu	class ·o

See definition df-omul 3107 for more information.

metamath.org