theorem :: NUMPOLY1:60

for n being non trivial Nat holds (Triangle n) + ((Triangle (n -' 1)) * (Triangle (n + 1))) = (Triangle n) |^ 2