let r be Real; :: thesis: for seq being Real_Sequence holds abs (r (#) seq) = |.r.| (#) (abs seq)
let seq be Real_Sequence; :: thesis: abs (r (#) seq) = |.r.| (#) (abs seq)

now :: thesis: for n being Element of NAT holds (abs (r (#) seq)) . n = (|.r.| (#) (abs seq)) . n

let n be Element of NAT ; :: thesis: (abs (r (#) seq)) . n = (|.r.| (#) (abs seq)) . n
thus (abs (r (#) seq)) . n = |.((r (#) seq) . n).| by Th12
.= |.(r * (seq . n)).| by Th9
.= |.r.| * |.(seq . n).| by COMPLEX1:65
.= |.r.| * ((abs seq) . n) by Th12
.= (|.r.| (#) (abs seq)) . n by Th9 ; :: thesis: verum

end;

hence abs (r (#) seq) = |.r.| (#) (abs seq) by FUNCT_2:63; :: thesis: verum