reconsider A = [.0,1.] as non empty real-membered set ;

deffunc H_{1}( Element of A, Element of A) -> Element of A = In ((1 - (t . ((1 - $1),(1 - $2)))),A);

ex f being Function of [:A,A:],A st

for x, y being Element of A holds f . (x,y) = H_{1}(x,y)
from BINOP_1:sch 4();

then consider f being BinOp of A such that

A1: for x, y being Element of A holds f . (x,y) = H_{1}(x,y)
;

reconsider ff = f as BinOp of [.0,1.] ;

take ff ; :: thesis: for a, b being Element of [.0,1.] holds ff . (a,b) = 1 - (t . ((1 - a),(1 - b)))

let a, b be Element of [.0,1.]; :: thesis: ff . (a,b) = 1 - (t . ((1 - a),(1 - b)))

reconsider aa = a, bb = b as Element of A ;

ff . (a,b) = H_{1}(aa,bb)
by A1;

hence ff . (a,b) = 1 - (t . ((1 - a),(1 - b))) by SUBSET_1:def 8, CoIn01; :: thesis: verum

deffunc H

ex f being Function of [:A,A:],A st

for x, y being Element of A holds f . (x,y) = H

then consider f being BinOp of A such that

A1: for x, y being Element of A holds f . (x,y) = H

reconsider ff = f as BinOp of [.0,1.] ;

take ff ; :: thesis: for a, b being Element of [.0,1.] holds ff . (a,b) = 1 - (t . ((1 - a),(1 - b)))

let a, b be Element of [.0,1.]; :: thesis: ff . (a,b) = 1 - (t . ((1 - a),(1 - b)))

reconsider aa = a, bb = b as Element of A ;

ff . (a,b) = H

hence ff . (a,b) = 1 - (t . ((1 - a),(1 - b))) by SUBSET_1:def 8, CoIn01; :: thesis: verum