deffunc H₁( Element of omega ) -> Element of VAR = x. (card $1);
thus for f1, f2 being Function of omega,VAR st ( for x being Element of omega holds f1 . x = H₁(x) ) & ( for x being Element of omega holds f2 . x = H₁(x) ) holds
f1 = f2 from BINOP_2:sch 1(); :: thesis: verum