let p be Function; :: thesis: ( dom p c= NAT implies for k being Element of NAT holds rng (Shift p,k) = rng p )
assume A1: 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 Th26; :: 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
A2: x in dom p and
A3: y = p . x by FUNCT_1:def 5;
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, Th25;
hence y in rng (Shift p,k) by FUNCT_1:def 5; :: thesis: verum