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

end;