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
dom (a * x) = dom x by VALUED_1:def 5;
hence len (a * x) = len x by FINSEQ_3:29; :: thesis: verum