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 19
.= (dom f) /\ (dom f)
.= dom f ;
A2: rng (((dom f) --> v) ** f) c= Y *

proof

let y be object ; :: 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 object such that
A3: x in dom (((dom f) --> v) ** f) and
A4: y = (((dom f) --> v) ** f) . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A1, A3;
f . x in X * by A1, A3, FINSEQ_2:11;
then A5: f . x is FinSequence of X by FINSEQ_1:def 11;
y = (((dom f) --> v) . x) * (f . x) by A3, A4, PBOOLE:def 19
.= v * (f . x) by A1, A3, FUNCOP_1:7 ;
then y is FinSequence of Y by A5, FINSEQ_2:32;
hence y in Y * by FINSEQ_1:def 11; :: thesis: verum

end;

dom (((dom f) --> v) ** f) = Seg (len f) by A1, FINSEQ_1:def 3;
then ((dom f) --> v) ** f is FinSequence-like by FINSEQ_1:def 2;
hence ((dom f) --> v) ** f is FinSequence of Y * by A2, FINSEQ_1:def 4; :: thesis: verum