let I be Program of SCM+FSA ; :: thesis: I +* (Start-At (insloc 0 )) c= Initialized I
( I c= Initialized I & Start-At (insloc 0 ) c= Initialized I ) by SCMFSA6A:26, SCMFSA6B:4;
hence I +* (Start-At (insloc 0 )) c= Initialized I by FUNCT_4:92; :: thesis: verum