let a be Real; :: thesis: for F being real-valued FinSequence holds len (a * F) = len F
let F be real-valued FinSequence; :: thesis: len (a * F) = len F
dom (a * F) = dom F by VALUED_1:def 5;
hence len (a * F) = len F by FINSEQ_3:29; :: thesis: verum