let X, Y be non empty set ; :: thesis: for f being FinSequence of X *
for v being Function of X,Y holds ((dom f) --> v) ** f is FinSequence of Y *
let f be FinSequence of X * ; :: thesis: for v being Function of X,Y holds ((dom f) --> v) ** f is FinSequence of Y *
let v be Function of X,Y; :: thesis: ((dom f) --> v) ** f is FinSequence of Y *
set F = ((dom f) --> v) ** f;
A1: dom (((dom f) --> v) ** f) = (dom ((dom f) --> v)) /\ (dom f) by PBOOLE:def 24
.= (dom f) /\ (dom f) by FUNCOP_1:19
.= dom f ;
then dom (((dom f) --> v) ** f) = Seg (len f) by FINSEQ_1:def 3;
then A2: ((dom f) --> v) ** f is FinSequence-like by FINSEQ_1:def 2;
rng (((dom f) --> v) ** f) c= Y *

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (((dom f) --> v) ** f) or y in Y * )
assume y in rng (((dom f) --> v) ** f) ; :: thesis: y in Y *
then consider x being set such that
A3: ( x in dom (((dom f) --> v) ** f) & y = (((dom f) --> v) ** f) . x ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A1, A3;
A4: y = (((dom f) --> v) . x) * (f . x) by A3, PBOOLE:def 24
.= v * (f . x) by A1, A3, FUNCOP_1:13 ;
f . x in X * by A1, A3, FINSEQ_2:13;
then f . x is FinSequence of X by FINSEQ_1:def 11;
then y is FinSequence of Y by A4, FINSEQ_2:36;
hence y in Y * by FINSEQ_1:def 11; :: thesis: verum

end;

hence ((dom f) --> v) ** f is FinSequence of Y * by A2, FINSEQ_1:def 4; :: thesis: verum