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