let p be Function; :: thesis: ( dom p c= NAT implies for k being Element of NAT holds rng (Shift p,k) = rng p )
assume Z: dom p c= NAT ; :: thesis: for k being Element of NAT holds rng (Shift p,k) = rng p
let k be Element of NAT ; :: thesis: rng (Shift p,k) = rng p
thus rng (Shift p,k) c= rng p by TW1; :: according to XBOOLE_0:def 10 :: thesis: rng p c= rng (Shift p,k)
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in rng (Shift p,k) )
assume y in rng p ; :: thesis: y in rng (Shift p,k)
then consider x being set such that
W1: x in dom p and
W2: y = p . x by FUNCT_1:def 5;
reconsider x = x as Element of NAT by W1, Z;
A: x + k in dom (Shift p,k) by TW2, W1;
(Shift p,k) . (x + k) = y by W1, W2, Def12;
hence y in rng (Shift p,k) by A, FUNCT_1:def 5; :: thesis: verum