let I be Program of SCM+FSA ; :: thesis: I c= Initialized I
set A = NAT ;
A1: dom I c= NAT by RELAT_1:def 18;
A2: not IC SCM+FSA in dom I by A1, AMI_1:48;
A3: not intloc 0 in dom I by A1, SCMFSA_2:84;
dom (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )) = (dom ((intloc 0 ) .--> 1)) \/ (dom (Start-At 0 ,SCM+FSA )) by FUNCT_4:def 1
.= {(intloc 0 )} \/ (dom (Start-At 0 ,SCM+FSA )) by FUNCOP_1:19
.= {(intloc 0 )} \/ {(IC SCM+FSA )} by FUNCOP_1:19
.= {(IC SCM+FSA ),(intloc 0 )} by ENUMSET1:41 ;
then ( Initialized I = I +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )) & dom I misses dom (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )) ) by A2, A3, FUNCT_4:15, ZFMISC_1:57;
hence I c= Initialized I by FUNCT_4:33; :: thesis: verum