( rng v c= A & rng (v * ll) c= rng v ) by RELAT_1:26, RELAT_1:def 19;
then A1: rng (v * ll) c= A by XBOOLE_1:1;
A2: len ll = k by CARD_1:def 7;
dom v = bound_QC-variables Al by FUNCT_2:def 1;
then rng ll c= dom v by RELAT_1:def 19;
then dom (v * ll) = dom ll by RELAT_1:27
.= Seg k by A2, FINSEQ_1:def 3 ;
then v * ll is FinSequence-like by FINSEQ_1:def 2;
hence *' is FinSequence of A by A1, FINSEQ_1:def 4; :: thesis: verum