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

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