let N be non empty with_non-empty_elements set ; :: thesis: for x being set
for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for I being Program of S st x in dom I holds
I . x = (I +* (Start-At (n,S))) . x
let x be set ; :: thesis: for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for I being Program of S st x in dom I holds
I . x = (I +* (Start-At (n,S))) . x
let n be Element of NAT ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for I being Program of S st x in dom I holds
I . x = (I +* (Start-At (n,S))) . x
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for I being Program of S st x in dom I holds
I . x = (I +* (Start-At (n,S))) . x
let I be Program of S; :: thesis: ( x in dom I implies I . x = (I +* (Start-At (n,S))) . x )
assume x in dom I ; :: thesis: I . x = (I +* (Start-At (n,S))) . x
then reconsider l = x as Element of NAT ;
( dom (Start-At (n,S)) = {(IC S)} & l <> IC S ) by Th3, FUNCOP_1:19;
then not x in dom (Start-At (n,S)) by TARSKI:def 1;
hence I . x = (I +* (Start-At (n,S))) . x by FUNCT_4:12; :: thesis: verum