let n be Element of NAT ; :: thesis: for I being Program of SCM+FSA
for s being State of SCM+FSA st I +* (Start-At n,SCM+FSA ) c= s holds
I c= s
let I be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA st I +* (Start-At n,SCM+FSA ) c= s holds
I c= s
let s be State of SCM+FSA ; :: thesis: ( I +* (Start-At n,SCM+FSA ) c= s implies I c= s )
dom I misses dom (Start-At n,SCM+FSA ) by SF_MASTR:64;
then A1: I +* (Start-At n,SCM+FSA ) = I \/ (Start-At n,SCM+FSA ) by FUNCT_4:32;
assume I +* (Start-At n,SCM+FSA ) c= s ; :: thesis: I c= s
hence I c= s by A1, XBOOLE_1:11; :: thesis: verum