theorem Th7: :: POLYFORM:8

for n being Nat st n is even holds
(- 1) |^ n = 1