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

now :: thesis: for n being Element of NAT holds (- H) . n = ((- 1) (#) H) . n

let n be Element of NAT ; :: thesis: (- H) . n = ((- 1) (#) H) . n
thus (- H) . n = - (H . n) by Def3
.= ((- 1) (#) H) . n by Def1 ; :: thesis: verum

end;

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