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 H1( 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 = 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 = 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 that A2:
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
and A3:
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
A4:
for
f,
g being
Element of
ModelSP (Inf_seq S) holds
o1 . f,
g = H1(
f,
g)
by A2;
for
f,
g being
Element of
ModelSP (Inf_seq S) holds
o2 . f,
g = H1(
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 = 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