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 = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g)) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o2 . f,g = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g)) ) 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) = (Not_ S) . ((Until_ S) . ((Not_ S) . $1),((Not_ S) . $2));
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 = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g)) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o2 . f,g = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g)) ) 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 = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g)) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o2 . f,g = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g)) ) implies o1 = o2 )
assume that
A2: for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o1 . f,g = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g)) and
A3: for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o2 . f,g = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g)) ; :: thesis: o1 = o2
A4: for f, g being Element of ModelSP (Inf_seq S) holds o1 . f,g = H₁(f,g) by A2;
for f, g being Element of ModelSP (Inf_seq S) holds o2 . f,g = H₁(f,g) by A3;
hence o1 = o2 by A4, 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 = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g)) ) & ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o2 . f,g = (Not_ S) . ((Until_ S) . ((Not_ S) . f),((Not_ S) . g)) ) holds
o1 = o2 ; :: thesis: verum