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