let S be non empty set ; :: thesis: ex o 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
o . f,g = (Not_ S) . ((And_ S) . ((Not_ S) . f),((Not_ S) . g))
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) . ((And_ S) . ((Not_ S) . $1),((Not_ S) . $2));
consider o being BinOp of (ModelSP (Inf_seq S)) such that
A1: for f, g being Element of ModelSP (Inf_seq S) holds o . f,g = H₁(f,g) from BINOP_1:sch 4();
for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o . f,g = (Not_ S) . ((And_ S) . ((Not_ S) . f),((Not_ S) . g)) by A1;
hence ex o 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
o . f,g = (Not_ S) . ((And_ S) . ((Not_ S) . f),((Not_ S) . g)) ; :: thesis: verum