dom v = bound_QC-variables by FUNCT_2:def 1;
then A1: rng ll c= dom v by CQC_LANG:def 5;
A2: len ll = k by QC_LANG1:def 8;
dom (v * ll) = dom ll by A1, RELAT_1:46
.= Seg k by A2, FINSEQ_1:def 3 ;
then A3: v * ll is FinSequence-like by FINSEQ_1:def 2;
A4: rng v c= A by RELSET_1:12;
rng (v * ll) c= rng v by RELAT_1:45;
then rng (v * ll) c= A by A4, XBOOLE_1:1;
hence v * ll is FinSequence of A by A3, FINSEQ_1:def 4; :: thesis: verum