let a be real number ; :: 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 Lm4;
then reconsider z = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:110;
len (a * z) = len x by FINSEQ_1:def 18;
hence len (a * x) = len x ; :: thesis: verum