let S be non empty set ; :: thesis: for R being total Relation of S,S
for o1, o2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o1 . (f,g) = EUntill_0 (f,g,R) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o2 . (f,g) = EUntill_0 (f,g,R) ) holds
o1 = o2
let R be total Relation of S,S; :: thesis: for o1, o2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o1 . (f,g) = EUntill_0 (f,g,R) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o2 . (f,g) = EUntill_0 (f,g,R) ) holds
o1 = o2
set M = ModelSP S;
deffunc H₁( Element of ModelSP S, Element of ModelSP S) -> Element of ModelSP S = EUntill_0 ($1,$2,R);
A1: for o1, o2 being BinOp of (ModelSP S) st ( for f, g being Element of ModelSP S holds o1 . (f,g) = H₁(f,g) ) & ( for f, g being Element of ModelSP S holds o2 . (f,g) = H₁(f,g) ) holds
o1 = o2 from BINOP_2:sch 2();
for o1, o2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o1 . (f,g) = EUntill_0 (f,g,R) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o2 . (f,g) = EUntill_0 (f,g,R) ) holds
o1 = o2

proof

let o1, o2 be BinOp of (ModelSP S); :: thesis: ( ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o1 . (f,g) = EUntill_0 (f,g,R) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o2 . (f,g) = EUntill_0 (f,g,R) ) implies o1 = o2 )
assume that
A2: for f, g being set st f in ModelSP S & g in ModelSP S holds
o1 . (f,g) = EUntill_0 (f,g,R) and
A3: for f, g being set st f in ModelSP S & g in ModelSP S holds
o2 . (f,g) = EUntill_0 (f,g,R) ; :: thesis: o1 = o2
A4: for f, g being Element of ModelSP S holds o2 . (f,g) = H₁(f,g) by A3;
for f, g being Element of ModelSP S holds o1 . (f,g) = H₁(f,g) by A2;
hence o1 = o2 by A1, A4; :: thesis: verum

end;

hence for o1, o2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o1 . (f,g) = EUntill_0 (f,g,R) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o2 . (f,g) = EUntill_0 (f,g,R) ) holds
o1 = o2 ; :: thesis: verum