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