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 = And_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 = And_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) = And_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 = And_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 = And_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 = And_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 = And_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 = And_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 = And_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 = And_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 = And_0 f,g,S ) holds
o1 = o2 ; :: thesis: verum