deffunc H1( object ) -> Element of BOOLEAN = AtomicFunc (a,$1);
A1:
for x being object st x in Inf_seq AtomicFamily holds
H1(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 = H1(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
; 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 ;
( t in Inf_seq AtomicFamily implies (Fid (IT,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t) )
assume A3:
t in Inf_seq AtomicFamily
;
(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)
;
verum
end;
hence
for t being set st t in Inf_seq AtomicFamily holds
(Fid (IT,(Inf_seq AtomicFamily))) . t = AtomicFunc (a,t)
; verum