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

let n be Element of NAT ; :: thesis: (abs (H " )) . n = ((abs H) " ) . n
thus (abs (H " )) . n = abs ((H " ) . n) by Def5
.= abs ((H . n) ^ ) by Def3
.= (abs (H . n)) ^ by RFUNCT_1:46
.= ((abs H) . n) ^ by Def5
.= ((abs H) " ) . n by Def3 ; :: thesis: verum

end;

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