let p be FinSequence; :: thesis: for x being object
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 object ; :: 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

A3: len (p |-- x) = (len p) - (x .. p) by A1, Def6;
let y be object ; :: 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 object such that
A4: z in dom (p |-- x) and
A5: (p |-- x) . z = y by FUNCT_1:def 3;
reconsider z = z as Element of NAT by A4;
dom (p |-- x) = Seg (len (p |-- x)) by FINSEQ_1:def 3;
then z <= len (p |-- x) by A4, FINSEQ_1:1;
then A6: z + (x .. p) <= len p by A3, XREAL_1:19;
1 <= z + (x .. p) by A1, Th21, NAT_1:12;
then z + (x .. p) in Seg (len p) by A6;
then A7: z + (x .. p) in dom p by FINSEQ_1:def 3;
y = p . (z + (x .. p)) by A1, A4, A5, Def6;
then A8: y in rng p by A7, FUNCT_1:def 3;
rng p c= D by A2, FINSEQ_1:def 4;
hence y in D by A8; :: thesis: verum

end;

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