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

now :: thesis: for n being Element of NAT holds (abs (r (#) H)) . n = (|.r.| (#) (abs H)) . n

let n be Element of NAT ; :: thesis: (abs (r (#) H)) . n = (|.r.| (#) (abs H)) . n
thus (abs (r (#) H)) . n = abs ((r (#) H) . n) by Def4
.= abs (r (#) (H . n)) by Def1
.= |.r.| (#) (abs (H . n)) by RFUNCT_1:25
.= |.r.| (#) ((abs H) . n) by Def4
.= (|.r.| (#) (abs H)) . n by Def1 ; :: thesis: verum

end;

hence abs (r (#) H) = |.r.| (#) (abs H) by FUNCT_2:63; :: thesis: verum