let p be Function; :: thesis: for k being Nat holds rng (Shift (p,k)) c= rng p
let k be Nat; :: thesis: rng (Shift (p,k)) c= rng p
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Shift (p,k)) or y in rng p )
assume y in rng (Shift (p,k)) ; :: thesis: y in rng p
then consider x being object such that
A1: x in dom (Shift (p,k)) and
A2: y = (Shift (p,k)) . x by FUNCT_1:def 3;
x in { (m + k) where m is Nat : m in dom p } by A1, Def12;
then consider m being Nat such that
A3: x = m + k and
A4: m in dom p ;
p . m = (Shift (p,k)) . x by A3, A4, Def12;
hence y in rng p by A2, A4, FUNCT_1:def 3; :: thesis: verum