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