let I be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA st Initialized I c= s holds
I c= s
let s be State of SCM+FSA ; :: thesis: ( Initialized I c= s implies I c= s )
dom I misses dom (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )) by Th2;
then A1: ( Initialized I = I +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )) & I +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )) = I \/ (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )) ) by FUNCT_4:15, FUNCT_4:32;
assume Initialized I c= s ; :: thesis: I c= s
hence I c= s by A1, XBOOLE_1:11; :: thesis: verum