theorem Th2: :: GRCAT_1:2

( op2 . ({},{}) = {} & op1 . {} = {} & op0 = {} )