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);
( ( 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)
;
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 ;
( 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
;
(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;
verum
end;
hence
f1 = f2
by Lm36, FUNCT_2:12;
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
; verum