let p be FinSequence; :: thesis: for x being object st x in rng p holds
rng (p |-- x) c= rng p
let x be object ; :: thesis: ( x in rng p implies rng (p |-- x) c= rng p )
assume A1: x in rng p ; :: thesis: rng (p |-- x) c= rng p
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (p |-- x) or y in rng p )
assume y in rng (p |-- x) ; :: thesis: y in rng p
then consider z being object such that
A2: z in dom (p |-- x) and
A3: (p |-- x) . z = y by FUNCT_1:def 3;
reconsider z = z as Element of NAT by A2;
( y = p . (z + (x .. p)) & z + (x .. p) in dom p ) by A1, A2, A3, Def6, Th43;
hence y in rng p by FUNCT_1:def 3; :: thesis: verum