let p be FinSequence; :: thesis: for x being set st x in rng p holds
rng (p |-- x) c= rng p
let x be set ; :: 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 set ; :: 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 set such that
A2: z in dom (p |-- x) and
A3: (p |-- x) . z = y by FUNCT_1:def 5;
reconsider z = z as Element of NAT by A2;
A4: y = p . (z + (x .. p)) by A1, A2, A3, Def7;
z + (x .. p) in dom p by A1, A2, Th58;
hence y in rng p by A4, FUNCT_1:def 5; :: thesis: verum