reconsider A = [.0,1.] as non empty real-membered set ;
deffunc H₁( Element of A, Element of A) -> Element of A = In ((min (($1 + $2),1)),A);
ex f being Function of [:A,A:],A st
for x, y being Element of A holds f . (x,y) = H₁(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₁(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) = min ((a + b),1)
let a, b be Element of [.0,1.]; :: thesis: ff . (a,b) = min ((a + b),1)
reconsider aa = a, bb = b as Element of A ;
ff . (a,b) = H₁(aa,bb) by A1;
hence ff . (a,b) = min ((a + b),1) by SUBSET_1:def 8, Lemma2a; :: thesis: verum