let I be Program of SCM+FSA ; :: thesis: for n being Element of NAT
for s being State of SCM+FSA st I +* (Start-At (insloc n)) c= s holds
IC s = insloc n
let n be Element of NAT ; :: thesis: for s being State of SCM+FSA st I +* (Start-At (insloc n)) c= s holds
IC s = insloc n
let s be State of SCM+FSA ; :: thesis: ( I +* (Start-At (insloc n)) c= s implies IC s = insloc n )
assume A1: I +* (Start-At (insloc n)) c= s ; :: thesis: IC s = insloc n
IC SCM+FSA in dom (I +* (Start-At (insloc n))) by Th65;
hence IC s = (I +* (Start-At (insloc n))) . (IC SCM+FSA ) by A1, GRFUNC_1:8
.= insloc n by Th66 ;
:: thesis: verum