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