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