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 b1 being Function st b1 = op1 holds
b1 is involutive ; :: thesis: verum