op1 is ()
_{1} being Function st b_{1} = op1 holds

b_{1} is involutive
; :: thesis: verum

proof

hence
for b
let a be Element of {0}; :: according to PARTIT_2:def 3 :: thesis: op1 . (op1 . a) = a

a = {} by TARSKI:def 1;

hence op1 . (op1 . a) = a by FUNCT_2:50; :: thesis: verum

end;a = {} by TARSKI:def 1;

hence op1 . (op1 . a) = a by FUNCT_2:50; :: thesis: verum

b