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 object st t in Inf_seq AtomicFamily holds
(Fid (f1,(Inf_seq AtomicFamily))) . t = (Fid (f2,(Inf_seq AtomicFamily))) . t

proof

let t be object ; :: 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 Lm36, FUNCT_2:12; :: thesis: verum

end;

hence for b₁, b₂ being Element of ModelSP (Inf_seq AtomicFamily) st ( for t being set st t in Inf_seq AtomicFamily holds
(Fid (b₁,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t) ) & ( for t being set st t in Inf_seq AtomicFamily holds
(Fid (b₂,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t) ) holds
b₁ = b₂ ; :: thesis: verum