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