let S be non empty set ; 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) . ((And_ 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) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) ) holds
o1 = o2
set M = ModelSP (Inf_seq S);
deffunc H1( 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)));
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) = H1(f,g) ) & ( for f, g being Element of ModelSP (Inf_seq S) holds o2 . (f,g) = H1(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) . ((And_ 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) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) ) holds
o1 = o2
proof
let o1,
o2 be
BinOp of
(ModelSP (Inf_seq S));
( ( for f, g being set st f in ModelSP (Inf_seq S) & g in ModelSP (Inf_seq S) holds
o1 . (f,g) = (Not_ S) . ((And_ 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) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) ) 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)
= (Not_ S) . ((And_ 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) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) ) )
;
o1 = o2
then
( ( for
f,
g being
Element of
ModelSP (Inf_seq S) holds
o1 . (
f,
g)
= H1(
f,
g) ) & ( for
f,
g being
Element of
ModelSP (Inf_seq S) holds
o2 . (
f,
g)
= H1(
f,
g) ) )
;
hence
o1 = o2
by A1;
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) . ((And_ 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) . ((And_ S) . (((Not_ S) . f),((Not_ S) . g))) ) holds
o1 = o2
; verum