let D be non empty set ; :: thesis: for G, H being Functional_Sequence of D,REAL holds abs (G (#) H) = (abs G) (#) (abs H)
let G, H be Functional_Sequence of D,REAL ; :: thesis: abs (G (#) H) = (abs G) (#) (abs H)

now

let n be Element of NAT ; :: thesis: (abs (G (#) H)) . n = ((abs G) (#) (abs H)) . n
thus (abs (G (#) H)) . n = abs ((G (#) H) . n) by Def5
.= abs ((G . n) (#) (H . n)) by Def8
.= (abs (G . n)) (#) (abs (H . n)) by RFUNCT_1:36
.= ((abs G) . n) (#) (abs (H . n)) by Def5
.= ((abs G) . n) (#) ((abs H) . n) by Def5
.= ((abs G) (#) (abs H)) . n by Def8 ; :: thesis: verum

end;

hence abs (G (#) H) = (abs G) (#) (abs H) by FUNCT_2:113; :: thesis: verum