let p be FinSequence; :: thesis: for x being set
for D being non empty set st x in rng p & p is FinSequence of D holds
p |-- x is FinSequence of D
let x be set ; :: thesis: for D being non empty set st x in rng p & p is FinSequence of D holds
p |-- x is FinSequence of D
let D be non empty set ; :: thesis: ( x in rng p & p is FinSequence of D implies p |-- x is FinSequence of D )
assume that
A1: x in rng p and
A2: p is FinSequence of D ; :: thesis: p |-- x is FinSequence of D
rng (p |-- x) c= D

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (p |-- x) or y in D )
assume y in rng (p |-- x) ; :: thesis: y in D
then consider z being set such that
A3: z in dom (p |-- x) and
A4: (p |-- x) . z = y by FUNCT_1:def 5;
A5: dom (p |-- x) = Seg (len (p |-- x)) by FINSEQ_1:def 3;
reconsider z = z as Element of NAT by A3;
A6: y = p . (z + (x .. p)) by A1, A3, A4, Def7;
( 1 <= x .. p & x .. p <= z + (x .. p) ) by A1, Th31, NAT_1:12;
then A7: 1 <= z + (x .. p) by XXREAL_0:2;
( z <= len (p |-- x) & len (p |-- x) = (len p) - (x .. p) ) by A1, A3, A5, Def7, FINSEQ_1:3;
then z + (x .. p) <= len p by XREAL_1:21;
then z + (x .. p) in Seg (len p) by A7;
then z + (x .. p) in dom p by FINSEQ_1:def 3;
then ( y in rng p & rng p c= D ) by A2, A6, FINSEQ_1:def 4, FUNCT_1:def 5;
hence y in D ; :: thesis: verum

end;

hence p |-- x is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum