let a be Complex; :: thesis: for x being complex-valued FinSequence holds len (a (#) x) = len x
let x be complex-valued FinSequence; :: thesis: len (a (#) x) = len x
set n = len x;
x is FinSequence of COMPLEX by Lm2;
then reconsider z = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider a9 = a as Element of COMPLEX by XCMPLX_0:def 2;
len (a9 * z) = len x by CARD_1:def 7;
hence len (a (#) x) = len x ; :: thesis: verum