let D be non empty set ; :: thesis: for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y holds - H = (- 1) (#) H
let Y be RealNormSpace; :: thesis: for H being Functional_Sequence of D, the carrier of Y holds - H = (- 1) (#) H
let H be Functional_Sequence of D, the carrier of Y; :: 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 VFUNCT_1:23
.= ((- 1) (#) H) . n by Def1 ; :: thesis: verum

end;

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