deffunc H₁( Element of {0,1,2}) -> Element of {0,1,2} = - $1;
ex f being UnOp of {0,1,2} st
for x being Element of {0,1,2} holds f . x = H₁(x) from FUNCT_2:sch 4();
hence ex b₁ being UnOp of {0,1,2} st
for a being Element of {0,1,2} holds b₁ . a = - a ; :: thesis: verum