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

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 Def10
.= |.(H . n).| . x by Def4
.= |.((H . n) . x).| by VALUED_1:18
.= |.((H # x) . n).| by Def10
.= (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 :: thesis: for n being Element of NAT holds ((- H) # x) . n = (- (H # x)) . n

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

end;

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