let a be Element of 1; :: according to OPOSET_1:def 3 :: thesis: op1 . (op1 . a) = a
a = {} by CARD_1:87, TARSKI:def 1;
hence op1 . (op1 . a) = a by CARD_1:87, FUNCT_2:65; :: thesis: verum