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 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 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 in dom g holds
Start-At (((IC g) + k),S) c= Relocated (g,k)
let k be Element of NAT ; :: thesis: ( IC in dom g implies Start-At (((IC g) + k),S) c= Relocated (g,k) )
assume A1: IC in dom g ; :: thesis: Start-At (((IC g) + k),S) c= Relocated (g,k)
A2: Start-At (((IC g) + k),S) = {[(IC ),((IC g) + k)]} by FUNCT_4:87;
A3: IC (Relocated (g,k)) = (IC g) + k by A1, Th120;
A4: IC in dom (Relocated (g,k)) by Th119;
A5: [(IC ),((IC g) + k)] in Relocated (g,k) by A4, A3, 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 A2, A5, TARSKI:def 1; :: thesis: verum

end;