deffunc H₁( object ) -> Element of BOOLEAN = AtomicFunc (a,$1);
A1: for x being object st x in Inf_seq AtomicFamily holds
H₁(x) in BOOLEAN ;
consider IT being Function of (Inf_seq AtomicFamily),BOOLEAN such that
A2: for x being object st x in Inf_seq AtomicFamily holds
IT . x = H₁(x) from FUNCT_2:sch 2(A1);
reconsider IT = IT as Element of Funcs ((Inf_seq AtomicFamily),BOOLEAN) by FUNCT_2:8;
reconsider IT = IT as Element of ModelSP (Inf_seq AtomicFamily) by MODELC_1:def 40;
take IT ; :: thesis: for t being set st t in Inf_seq AtomicFamily holds
(Fid (IT,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t)
for t being set st t in Inf_seq AtomicFamily holds
(Fid (IT,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t)

proof

reconsider IT = IT as Function of (Inf_seq AtomicFamily),BOOLEAN ;
let t be set ; :: thesis: ( t in Inf_seq AtomicFamily implies (Fid (IT,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t) )
assume A3: t in Inf_seq AtomicFamily ; :: thesis: (Fid (IT,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t)
(Fid (IT,(Inf_seq AtomicFamily))) . t = IT . t by MODELC_1:def 41
.= AtomicFunc (a,t) by A2, A3 ;
hence (Fid (IT,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t) ; :: thesis: verum

end;

hence for t being set st t in Inf_seq AtomicFamily holds
(Fid (IT,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t) ; :: thesis: verum