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

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

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

end;

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