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

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

let n be Element of NAT ; :: thesis: (abs (H ")) . n = ((abs H) ") . n
thus (abs (H ")) . n = abs ((H ") . n) by Def4
.= abs ((H . n) ^) by Def2
.= (abs (H . n)) ^ by RFUNCT_1:30
.= ((abs H) . n) ^ by Def4
.= ((abs H) ") . n by Def2 ; :: thesis: verum

end;

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