for f1, f2 being Element of ModelSP (Inf_seq AtomicFamily ) st ( for t being set st t in Inf_seq AtomicFamily holds
(Fid f1,(Inf_seq AtomicFamily )) . t = AtomicFunc a,t ) & ( for t being set st t in Inf_seq AtomicFamily holds
(Fid f2,(Inf_seq AtomicFamily )) . t = AtomicFunc a,t ) holds
f1 = f2
proof
let f1,
f2 be
Element of
ModelSP (Inf_seq AtomicFamily );
:: thesis: ( ( for t being set st t in Inf_seq AtomicFamily holds
(Fid f1,(Inf_seq AtomicFamily )) . t = AtomicFunc a,t ) & ( for t being set st t in Inf_seq AtomicFamily holds
(Fid f2,(Inf_seq AtomicFamily )) . t = AtomicFunc a,t ) implies f1 = f2 )
assume that B1:
for
t being
set st
t in Inf_seq AtomicFamily holds
(Fid f1,(Inf_seq AtomicFamily )) . t = AtomicFunc a,
t
and B2:
for
t being
set st
t in Inf_seq AtomicFamily holds
(Fid f2,(Inf_seq AtomicFamily )) . t = AtomicFunc a,
t
;
:: thesis: f1 = f2
Fid f1,
(Inf_seq AtomicFamily ) = Fid f2,
(Inf_seq AtomicFamily )
proof
for
t being
set st
t in Inf_seq AtomicFamily holds
(Fid f1,(Inf_seq AtomicFamily )) . t = (Fid f2,(Inf_seq AtomicFamily )) . t
proof
let t be
set ;
:: thesis: ( t in Inf_seq AtomicFamily implies (Fid f1,(Inf_seq AtomicFamily )) . t = (Fid f2,(Inf_seq AtomicFamily )) . t )
assume C1:
t in Inf_seq AtomicFamily
;
:: thesis: (Fid f1,(Inf_seq AtomicFamily )) . t = (Fid f2,(Inf_seq AtomicFamily )) . t
(Fid f1,(Inf_seq AtomicFamily )) . t = AtomicFunc a,
t
by B1, C1;
hence
(Fid f1,(Inf_seq AtomicFamily )) . t = (Fid f2,(Inf_seq AtomicFamily )) . t
by B2, C1;
:: thesis: verum
end;
hence
Fid f1,
(Inf_seq AtomicFamily ) = Fid f2,
(Inf_seq AtomicFamily )
by FUNCT_2:18;
:: thesis: verum
end;
hence
f1 = f2
by LemFid;
:: thesis: verum
end;
hence
for b1, b2 being Element of ModelSP (Inf_seq AtomicFamily ) st ( for t being set st t in Inf_seq AtomicFamily holds
(Fid b1,(Inf_seq AtomicFamily )) . t = AtomicFunc a,t ) & ( for t being set st t in Inf_seq AtomicFamily holds
(Fid b2,(Inf_seq AtomicFamily )) . t = AtomicFunc a,t ) holds
b1 = b2
; :: thesis: verum