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 ;
dom EI c= NAT by RELAT_1:60, XBOOLE_1:2;
then reconsider EI = EI as Program of SCM+FSA by A1, RELAT_1:def 18, SCMNORM:def 1;
(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 (s +* ((intloc 0 ) .--> 1)) +* (Start-At 0 ,SCM+FSA ) is State of SCM+FSA ; :: thesis: verum