let I be Program of SCM+FSA ; :: thesis: I c= Initialized I
set A = NAT ;
A1: Initialized I = I +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:15;
A2: dom I c= NAT by RELAT_1:def 18;

A3: now

assume IC SCM+FSA in dom I ; :: thesis: contradiction
then reconsider l = IC SCM+FSA as Instruction-Location of SCM+FSA by A2, AMI_1:def 4;
l = IC SCM+FSA ;
hence contradiction by AMI_1:48; :: thesis: verum

end;

A4: now

assume intloc 0 in dom I ; :: thesis: contradiction
then reconsider l = intloc 0 as Instruction-Location of SCM+FSA by A2, AMI_1:def 4;
l = intloc 0 ;
hence contradiction by SCMFSA_2:84; :: thesis: verum

end;

dom (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) = (dom ((intloc 0 ) .--> 1)) \/ (dom (Start-At (insloc 0 ))) by FUNCT_4:def 1
.= {(intloc 0 )} \/ (dom (Start-At (insloc 0 ))) by FUNCOP_1:19
.= {(intloc 0 )} \/ {(IC SCM+FSA )} by FUNCOP_1:19
.= {(IC SCM+FSA ),(intloc 0 )} by ENUMSET1:41 ;
then dom I misses dom (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by A3, A4, ZFMISC_1:57;
hence I c= Initialized I by A1, FUNCT_4:33; :: thesis: verum