let D be non empty set ; :: thesis: for H being Functional_Sequence of D,REAL holds - (- H) = H
let H be Functional_Sequence of D,REAL ; :: thesis: - (- H) = H
thus - (- H) = (- 1) (#) (- H) by Th8
.= (- 1) (#) ((- 1) (#) H) by Th8
.= ((- 1) * (- 1)) (#) H by Th11
.= H by Th12 ; :: thesis: verum