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 :: thesis: for n being Element of NAT holds (abs (G (#) H)) . n = ((abs G) (#) (abs H)) . n

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 Def4
.= abs ((G . n) (#) (H . n)) by Def7
.= (abs (G . n)) (#) (abs (H . n)) by RFUNCT_1:24
.= ((abs G) . n) (#) (abs (H . n)) by Def4
.= ((abs G) . n) (#) ((abs H) . n) by Def4
.= ((abs G) (#) (abs H)) . n by Def7 ; :: thesis: verum

end;

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