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