let I be Program of SCM+FSA ; :: thesis: I +* (Start-At (insloc 0 )) c= Initialized I
set SA = Start-At (insloc 0 );
A1: Start-At (insloc 0 ) c= Initialized I by FUNCT_4:26;
I c= Initialized I by SCMFSA6A:26;
then A2: I \/ (Start-At (insloc 0 )) c= Initialized I by A1, XBOOLE_1:8;
I +* (Start-At (insloc 0 )) c= I \/ (Start-At (insloc 0 )) by FUNCT_4:30;
hence I +* (Start-At (insloc 0 )) c= Initialized I by A2, XBOOLE_1:1; :: thesis: verum