let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for g being FinPartState of S
for k being Element of NAT st IC S in dom g holds
Start-At (((IC g) + k),S) c= Relocated (g,k)
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N; :: thesis: for g being FinPartState of S
for k being Element of NAT st IC S in dom g holds
Start-At (((IC g) + k),S) c= Relocated (g,k)
let g be FinPartState of S; :: thesis: for k being Element of NAT st IC S in dom g holds
Start-At (((IC g) + k),S) c= Relocated (g,k)
let k be Element of NAT ; :: thesis: ( IC S in dom g implies Start-At (((IC g) + k),S) c= Relocated (g,k) )
assume Z: IC S in dom g ; :: thesis: Start-At (((IC g) + k),S) c= Relocated (g,k)
A1: Start-At (((IC g) + k),S) = {[(IC S),((IC g) + k)]} by FUNCT_4:87;
A2: IC (Relocated (g,k)) = (IC g) + k by Z, Th73;
A3: IC S in dom (Relocated (g,k)) by Th119;
A4: [(IC S),((IC g) + k)] in Relocated (g,k) by A3, A2, FUNCT_1:def 4;
thus Start-At (((IC g) + k),S) c= Relocated (g,k) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Start-At (((IC g) + k),S) or x in Relocated (g,k) )
assume x in Start-At (((IC g) + k),S) ; :: thesis: x in Relocated (g,k)
hence x in Relocated (g,k) by A1, A4, TARSKI:def 1; :: thesis: verum

end;