let I be non empty Program of SCM+FSA ; :: thesis: ( insloc 0 in dom I & insloc 0 in dom (Initialized I) & insloc 0 in dom (I +* (Start-At (insloc 0 ))) )
consider iloc being set such that
A1: iloc in dom I by XBOOLE_0:def 1;
dom I c= NAT by RELAT_1:def 18;
then reconsider iloc = iloc as Instruction-Location of SCM+FSA by A1, AMI_1:def 4;
reconsider i = iloc as Element of NAT by ORDINAL1:def 13;
( 0 < i or 0 = i ) ;
hence A3: insloc 0 in dom I by A1, SCMNORM:def 1; :: thesis: ( insloc 0 in dom (Initialized I) & insloc 0 in dom (I +* (Start-At (insloc 0 ))) )
I c= Initialized I by SCMFSA6A:26;
then dom I c= dom (Initialized I) by RELAT_1:25;
hence insloc 0 in dom (Initialized I) by A3; :: thesis: insloc 0 in dom (I +* (Start-At (insloc 0 )))
dom (I +* (Start-At (insloc 0 ))) = (dom I) \/ (dom (Start-At (insloc 0 ))) by FUNCT_4:def 1;
hence insloc 0 in dom (I +* (Start-At (insloc 0 ))) by A3, XBOOLE_0:def 3; :: thesis: verum