theorem :: NUMPOLY1:69

for n, m being non trivial Nat holds ((Triangle n) * (Triangle m)) + ((Triangle (n -' 1)) * (Triangle (m -' 1))) = Triangle (n * m)