let S be non empty set ; :: thesis: for R being total Relation of S,S ex o being BinOp of (ModelSP S) st
for f, g being set st f in ModelSP S & g in ModelSP S holds
o . (f,g) = EUntill_0 (f,g,R)
let R be total Relation of S,S; :: thesis: ex o being BinOp of (ModelSP S) st
for f, g being set st f in ModelSP S & g in ModelSP S holds
o . (f,g) = EUntill_0 (f,g,R)
set M = ModelSP S;
deffunc H₁( Element of ModelSP S, Element of ModelSP S) -> Element of ModelSP S = EUntill_0 ($1,$2,R);
consider o being BinOp of (ModelSP S) such that
A1: for f, g being Element of ModelSP S holds o . (f,g) = H₁(f,g) from BINOP_1:sch 4();
for f, g being set st f in ModelSP S & g in ModelSP S holds
o . (f,g) = EUntill_0 (f,g,R) by A1;
hence ex o being BinOp of (ModelSP S) st
for f, g being set st f in ModelSP S & g in ModelSP S holds
o . (f,g) = EUntill_0 (f,g,R) ; :: thesis: verum