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

now

let n be Element of NAT ; :: thesis: ((abs H) # x) . n = (abs (H # x)) . n
thus ((abs H) # x) . n = ((abs H) . n) . x by Def11
.= (abs (H . n)) . x by Def5
.= abs ((H . n) . x) by VALUED_1:18
.= abs ((H # x) . n) by Def11
.= (abs (H # x)) . n by SEQ_1:12 ; :: thesis: verum

end;

hence (abs H) # x = abs (H # x) by FUNCT_2:63; :: thesis: (- H) # x = - (H # x)

now

let n be Element of NAT ; :: thesis: ((- H) # x) . n = (- (H # x)) . n
thus ((- H) # x) . n = ((- H) . n) . x by Def11
.= (- (H . n)) . x by Def4
.= - ((H . n) . x) by VALUED_1:8
.= - ((H # x) . n) by Def11
.= (- (H # x)) . n by SEQ_1:10 ; :: thesis: verum

end;

hence (- H) # x = - (H # x) by FUNCT_2:63; :: thesis: verum