take (- 1) (#) H ; :: thesis: for n being Nat holds ((- 1) (#) H) . n = - (H . n)
let n be Nat; :: thesis: ((- 1) (#) H) . n = - (H . n)
for n being Nat holds ((- 1) (#) H) . n = - (H . n)

proof

let n be Nat; :: thesis: ((- 1) (#) H) . n = - (H . n)
thus ((- 1) (#) H) . n = (- 1) (#) (H . n) by Def1
.= - (H . n) by VFUNCT_1:23 ; :: thesis: verum

end;

hence ((- 1) (#) H) . n = - (H . n) ; :: thesis: verum