let a be real number ; :: 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:110;
len (a * G) = len G by FINSEQ_1:def 18;
hence len (a * F) = len F ; :: thesis: verum