deffunc H₁( Element of Funcs (A,REAL), Element of Funcs (A,REAL)) -> Element of Funcs (A,REAL) = maxreal .: ($1,$2);
ex o being BinOp of (Funcs (A,REAL)) st
for a, b being Element of Funcs (A,REAL) holds o . (a,b) = H₁(a,b) from BINOP_1:sch 4();
hence ex b₁ being BinOp of (Funcs (A,REAL)) st
for f, g being Element of Funcs (A,REAL) holds b₁ . (f,g) = maxreal .: (f,g) ; :: thesis: verum