let a be Real; :: thesis: for F being FinSequence of REAL holds len (a * F) = len F
let F be FinSequence of REAL ; :: thesis: len (a * F) = len F
reconsider G = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
len (a * G) = len G by CARD_1:def 7;
hence len (a * F) = len F ; :: thesis: verum