let I be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA st Initialized I c= s holds
I +* (Start-At (insloc 0 )) c= s
let s be State of SCM+FSA ; :: thesis: ( Initialized I c= s implies I +* (Start-At (insloc 0 )) c= s )
assume A1: Initialized I c= s ; :: thesis: I +* (Start-At (insloc 0 )) c= s
Start-At (insloc 0 ) c= Initialized I by FUNCT_4:26;
then A2: Start-At (insloc 0 ) c= s by A1, XBOOLE_1:1;
I c= Initialized I by SCMFSA6A:26;
then A3: I c= s by A1, XBOOLE_1:1;
dom I misses dom (Start-At (insloc 0 )) by SF_MASTR:64;
then I +* (Start-At (insloc 0 )) = I \/ (Start-At (insloc 0 )) by FUNCT_4:32;
hence I +* (Start-At (insloc 0 )) c= s by A2, A3, XBOOLE_1:8; :: thesis: verum