deffunc H₁( object ) -> Element of ModelSP (Inf_seq AtomicFamily) = AtomicAsgn $1;
A1: for a being object st a in atomic_LTL holds
H₁(a) in the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) ;
consider IT being Function of atomic_LTL, the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) such that
A2: for a being object st a in atomic_LTL holds
IT . a = H₁(a) from FUNCT_2:sch 2(A1);
take IT ; :: thesis: for a being set st a in atomic_LTL holds
IT . a = AtomicAsgn a
thus for a being set st a in atomic_LTL holds
IT . a = AtomicAsgn a by A2; :: thesis: verum