let r be real number ; :: thesis: for seq being Real_Sequence holds abs (r (#) seq) = (abs r) (#) (abs seq)
let seq be Real_Sequence; :: thesis: abs (r (#) seq) = (abs r) (#) (abs seq)

now

let n be Element of NAT ; :: thesis: (abs (r (#) seq)) . n = ((abs r) (#) (abs seq)) . n
thus (abs (r (#) seq)) . n = abs ((r (#) seq) . n) by Th16
.= abs (r * (seq . n)) by Th13
.= (abs r) * (abs (seq . n)) by COMPLEX1:151
.= (abs r) * ((abs seq) . n) by Th16
.= ((abs r) (#) (abs seq)) . n by Th13 ; :: thesis: verum

end;

hence abs (r (#) seq) = (abs r) (#) (abs seq) by FUNCT_2:113; :: thesis: verum