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 in dom I by A1, COMPOS_1:3;
A3: not intloc 0 in dom I by A1, SCMFSA_2:84;
dom (Initialize ((intloc 0) .--> 1)) = (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 )} by FUNCOP_1:19
.= {(IC ),(intloc 0)} by ENUMSET1:41 ;
then dom I misses dom (Initialize ((intloc 0) .--> 1)) by A2, A3, ZFMISC_1:57;
hence I c= Initialized I by FUNCT_4:33; :: thesis: verum