let seq, seq' be Real_Sequence; :: thesis: abs (seq (#) seq') = (abs seq) (#) (abs seq')

now

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

end;

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