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:86, XREAL_1:63;
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:58
.= sqrt (((abs r) ^2) * (Sum (sqr (abs x)))) by RVSUM_1:87
.= (sqrt ((abs r) ^2)) * (sqrt (Sum (sqr (abs x)))) by A1, SQUARE_1:29
.= (abs r) * (sqrt (Sum (sqr (abs x)))) by COMPLEX1:46, SQUARE_1:22
.= (abs r) * |.f.| by Lm3 ; :: thesis: verum