let s be State of ; :: thesis: for I being Program of
for a being Int-Location
for l being Instruction-Location of SCM+FSA holds (s +* (I +* (Start-At l))) . a = s . a
let I be Program of ; :: thesis: for a being Int-Location
for l being Instruction-Location of SCM+FSA holds (s +* (I +* (Start-At l))) . a = s . a
let a be Int-Location ; :: thesis: for l being Instruction-Location of SCM+FSA holds (s +* (I +* (Start-At l))) . a = s . a
let l be Instruction-Location of SCM+FSA ; :: thesis: (s +* (I +* (Start-At l))) . a = s . a
not a in dom (I +* (Start-At l)) by SCMFSA6B:12;
hence (s +* (I +* (Start-At l))) . a = s . a by FUNCT_4:12; :: thesis: verum