let p be FinPartState of SCM ; :: thesis: for k being Element of NAT holds Start-At ((IC p) + k) c= Relocated p,k
let k be Element of NAT ; :: thesis: Start-At ((IC p) + k) c= Relocated p,k
A1: Start-At ((IC p) + k) = {[(IC SCM ),((IC p) + k)]} by FUNCT_4:87;
A2: IC SCM in dom (Relocated p,k) by Th25;
A3: IC (Relocated p,k) = (IC p) + k by Th26;
IC (Relocated p,k) = (Relocated p,k) . (IC SCM ) by A2, AMI_1:def 43;
then A4: [(IC SCM ),((IC p) + k)] in Relocated p,k by A2, A3, FUNCT_1:def 4;
thus Start-At ((IC p) + k) 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) or x in Relocated p,k )
assume x in Start-At ((IC p) + k) ; :: thesis: x in Relocated p,k
hence x in Relocated p,k by A1, A4, TARSKI:def 1; :: thesis: verum

end;