let p be Function; for k being Nat holds rng (Shift (p,k)) c= rng p
let k be Nat; rng (Shift (p,k)) c= rng p
let y be object ; TARSKI:def 3 ( not y in rng (Shift (p,k)) or y in rng p )
assume
y in rng (Shift (p,k))
; 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; verum