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

proof

let o1, o2 be BinOp of (ModelSP (Inf_seq S)); :: thesis: ( ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o1 . (f,g) = Until_0 (f,g,S) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o2 . (f,g) = Until_0 (f,g,S) ) implies o1 = o2 )
assume ( ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o1 . (f,g) = Until_0 (f,g,S) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o2 . (f,g) = Until_0 (f,g,S) ) ) ; :: thesis: o1 = o2
then ( ( for f, g being Element of ModelSP (Inf_seq S) holds o1 . (f,g) = H₁(f,g) ) & ( for f, g being Element of ModelSP (Inf_seq S) holds o2 . (f,g) = H₁(f,g) ) ) ;
hence o1 = o2 by A1; :: thesis: verum

end;

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