let r be real number ; :: thesis: for f being real-valued FinSequence holds |.(r * f).| = (abs r) * |.f.|
let f be real-valued FinSequence; :: thesis: |.(r * f).| = (abs r) * |.f.|
set n = len f;
reconsider x = f as Element of REAL (len f) by Lm2;
A1: ( 0 <= (abs r) ^2 & 0 <= Sum (sqr (abs x)) ) by RVSUM_1:116, XREAL_1:65;
thus |.(r * f).| = sqrt (Sum (sqr (abs (r * x)))) by Lm3
.= sqrt (Sum (sqr ((abs r) * (abs x)))) by Th9
.= sqrt (Sum (((abs r) ^2 ) * (sqr (abs x)))) by RVSUM_1:84
.= sqrt (((abs r) ^2 ) * (Sum (sqr (abs x)))) by RVSUM_1:117
.= (sqrt ((abs r) ^2 )) * (sqrt (Sum (sqr (abs x)))) by A1, SQUARE_1:97
.= (abs r) * (sqrt (Sum (sqr (abs x)))) by COMPLEX1:132, SQUARE_1:89
.= (abs r) * |.f.| by Lm3 ; :: thesis: verum