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 A4:
for
t being
set st
t in Inf_seq AtomicFamily holds
(Fid f1,(Inf_seq AtomicFamily )) . t = AtomicFunc a,
t
and A5:
for
t being
set st
t in Inf_seq AtomicFamily holds
(Fid f2,(Inf_seq AtomicFamily )) . t = AtomicFunc a,
t
;
:: thesis: f1 = f2
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 A6:
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 A4, A6;
hence
(Fid f1,(Inf_seq AtomicFamily )) . t = (Fid f2,(Inf_seq AtomicFamily )) . t
by A5, A6;
:: thesis: verum
end;
hence
f1 = f2
by Lm43, FUNCT_2:18;
:: 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