op1 is ()

proof

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;

hence for b₁ being Function st b₁ = op1 holds
b₁ is involutive ; :: thesis: verum