theorem :: NUMPOLY1:63

for n being non zero Nat holds (3 * (Triangle n)) + (Triangle (n -' 1)) = Triangle (2 * n)