deffunc H₁( Element of Funcs A,REAL , Element of Funcs A,REAL ) -> Element of Funcs A,REAL = minreal .: $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 = minreal .: f,g ; :: thesis: verum