let a be Real; :: thesis: for x being real-valued FinSequence holds len (a * x) = len x
let x be real-valued FinSequence; :: thesis: len (a * x) = len x
set n = len x;
x is FinSequence of REAL by Lm2;
then reconsider z = x as Element of (len x) -tuples_on REAL by FINSEQ_2:92;
len (a * z) = len x by CARD_1:def 7;
hence len (a * x) = len x ; :: thesis: verum