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