reconsider EI = {} as FinPartState of SCM+FSA by FUNCT_1:174, RELAT_1:206;
A1: for m, n being Nat st n in dom EI & m < n holds
m in dom EI ;
X: rng EI c= the Instructions of SCM+FSA by RELAT_1:60, XBOOLE_1:2;
dom EI c= NAT by RELAT_1:60, XBOOLE_1:2;
then reconsider EI = EI as Program of SCM+FSA by A1, X, AFINSQ_1:def 13, RELAT_1:def 18, RELAT_1:def 19;
(s +* ((intloc 0 ) .--> 1)) +* (Start-At 0 ,SCM+FSA ) = ((s +* EI) +* ((intloc 0 ) .--> 1)) +* (Start-At 0 ,SCM+FSA ) by FUNCT_4:22
.= (s +* EI) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:15
.= s +* (EI +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))) by FUNCT_4:15
.= s +* (Initialized EI) by FUNCT_4:15 ;
hence Initialized s is total ; :: thesis: verum