let p be Function; :: thesis: ( dom p c= NAT implies for k being Nat holds rng (Shift (p,k)) = rng p )
assume A1: dom p c= NAT ; :: thesis: for k being Nat holds rng (Shift (p,k)) = rng p
let k be Nat; :: thesis: rng (Shift (p,k)) = rng p
thus rng (Shift (p,k)) c= rng p by Th25; :: according to XBOOLE_0:def 10 :: thesis: rng p c= rng (Shift (p,k))
let y be object ; :: 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 object such that
A2: x in dom p and
A3: y = p . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A1, A2;
( x + k in dom (Shift (p,k)) & (Shift (p,k)) . (x + k) = y ) by A2, A3, Def12, Th24;
hence y in rng (Shift (p,k)) by FUNCT_1:def 3; :: thesis: verum