deffunc H₁( Real, Real) -> set = (h ") . (f . ((h . $1),(h . $2)));
A1: for a, b being Element of [.0,1.] holds H₁(a,b) in [.0,1.]

proof

let a, b be Element of [.0,1.]; :: thesis: H₁(a,b) in [.0,1.]
(h ") . (f . ((h . a),(h . b))) in [.0,1.] ;
hence H₁(a,b) in [.0,1.] ; :: thesis: verum

end;

ex f being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds f . (a,b) = H₁(a,b) from FUZNORM1:sch 1(A1);
hence ex b₁ being BinOp of [.0,1.] st
for x1, x2 being Element of [.0,1.] holds b₁ . (x1,x2) = (h ") . (f . ((h . x1),(h . x2))) ; :: thesis: verum