let p be Function; :: thesis: for k being Element of NAT holds rng (Shift p,k) c= rng p
let k be Element of NAT ; :: thesis: rng (Shift p,k) c= rng p
let y be set ; :: 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 set such that
W1: x in dom (Shift p,k) and
W2: y = (Shift p,k) . x by FUNCT_1:def 5;
x in { (m + k) where m is Element of NAT : m in dom p } by W1, Def12;
then consider m being Element of NAT such that
W4: x = m + k and
W3: m in dom p ;
p . m = (Shift p,k) . x by W3, W4, Def12;
hence y in rng p by W3, W2, FUNCT_1:def 5; :: thesis: verum