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 SF_MASTR:64;
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