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

now

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

end;

hence abs (seq (#) seq9) = (abs seq) (#) (abs seq9) by FUNCT_2:63; :: thesis: verum