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, COMPOS_1:3;
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