let p be FinPartState of SCM+FSA ; :: thesis: for k being Element of NAT holds Start-At ((IC p) + k),SCM+FSA c= Relocated p,k
let k be Element of NAT ; :: thesis: Start-At ((IC p) + k),SCM+FSA c= Relocated p,k
A1: Start-At ((IC p) + k),SCM+FSA = {[(IC SCM+FSA ),((IC p) + k)]} by FUNCT_4:87;
A2: IC (Relocated p,k) = (IC p) + k by Th6;
A3: IC SCM+FSA in dom (Relocated p,k) by Th5;
A4: [(IC SCM+FSA ),((IC p) + k)] in Relocated p,k by A3, A2, FUNCT_1:def 4;
thus Start-At ((IC p) + k),SCM+FSA c= Relocated p,k :: thesis: verum

proof

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

end;