let n be Element of NAT ; :: thesis: for x being set
for I being Program of SCM+FSA st x in dom I holds
I . x = (I +* (Start-At n,SCM+FSA )) . x
let x be set ; :: thesis: for I being Program of SCM+FSA st x in dom I holds
I . x = (I +* (Start-At n,SCM+FSA )) . x
let I be Program of SCM+FSA ; :: thesis: ( x in dom I implies I . x = (I +* (Start-At n,SCM+FSA )) . x )
A1: dom I c= NAT by RELAT_1:def 18;
assume x in dom I ; :: thesis: I . x = (I +* (Start-At n,SCM+FSA )) . x
then ( dom (Start-At n,SCM+FSA ) = {(IC SCM+FSA )} & x <> IC SCM+FSA ) by A1, Lm1, FUNCOP_1:19;
then not x in dom (Start-At n,SCM+FSA ) by TARSKI:def 1;
hence I . x = (I +* (Start-At n,SCM+FSA )) . x by FUNCT_4:12; :: thesis: verum