let a be complex number ; :: thesis: for x being FinSequence of COMPLEX holds len (a * x) = len x
let x be FinSequence of COMPLEX ; :: thesis: len (a * x) = len x
set n = len x;
reconsider z = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider a' = a as Element of COMPLEX by XCMPLX_0:def 2;
len (a' * z) = len x by FINSEQ_1:def 18;
hence len (a * x) = len x ; :: thesis: verum