let r be real number ; :: thesis: for f being real-valued FinSequence holds abs (r * f) = (abs r) * (abs f)
let f be real-valued FinSequence; :: thesis: abs (r * f) = (abs r) * (abs f)
set n = len f;
reconsider n = len f as Element of NAT ;
reconsider x = f as Element of REAL n by Lm2;

now

let j be Nat; :: thesis: ( j in Seg n implies (abs (r * x)) . j = ((abs r) * (abs x)) . j )
assume j in Seg n ; :: thesis: (abs (r * x)) . j = ((abs r) * (abs x)) . j
reconsider r' = x . j, rr = (r * x) . j as Element of REAL ;
reconsider ar = (abs x) . j as Real ;
thus (abs (r * x)) . j = abs rr by Th6
.= abs (r * r') by RVSUM_1:66
.= (abs r) * (abs r') by COMPLEX1:151
.= (abs r) * ar by Th6
.= ((abs r) * (abs x)) . j by RVSUM_1:67 ; :: thesis: verum

end;

hence abs (r * f) = (abs r) * (abs f) by FINSEQ_2:139; :: thesis: verum