let n, m be non trivial Nat; ((Triangle n) * (Triangle m)) + ((Triangle (n -' 1)) * (Triangle (m -' 1))) = Triangle (n * m)
0 + 1 <= n
by NAT_1:13;
then A1:
n -' 1 = n - 1
by XREAL_1:233;
0 + 1 <= m
by NAT_1:13;
then A2:
m -' 1 = m - 1
by XREAL_1:233;
A3:
Triangle (n -' 1) = ((n - 1) * ((n - 1) + 1)) / 2
by A1, Th19;
A4:
Triangle (m -' 1) = ((m - 1) * ((m - 1) + 1)) / 2
by A2, Th19;
A5:
Triangle (n * m) = ((n * m) * ((n * m) + 1)) / 2
by Th19;
((Triangle n) * (Triangle m)) + ((Triangle (n -' 1)) * (Triangle (m -' 1))) =
(((n * (n + 1)) / 2) * (Triangle m)) + ((Triangle (n -' 1)) * (Triangle (m -' 1)))
by Th19
.=
(((n * (n + 1)) / 2) * ((m * (m + 1)) / 2)) + ((((n - 1) * ((n - 1) + 1)) / 2) * (((m - 1) * ((m - 1) + 1)) / 2))
by A4, A3, Th19
.=
((((n * n) + n) / 2) * (((m * m) + m) / 2)) + ((((n * n) - n) / 2) * (((m * m) - m) / 2))
.=
((((n |^ 2) + n) / 2) * (((m * m) + m) / 2)) + ((((n * n) - n) / 2) * (((m * m) - m) / 2))
by NEWTON:81
.=
((((n |^ 2) + n) / 2) * (((m |^ 2) + m) / 2)) + ((((n * n) - n) / 2) * (((m * m) - m) / 2))
by NEWTON:81
.=
((((n |^ 2) + n) / 2) * (((m |^ 2) + m) / 2)) + ((((n |^ 2) - n) / 2) * (((m * m) - m) / 2))
by NEWTON:81
.=
((((n |^ 2) + n) / 2) * (((m |^ 2) + m) / 2)) + ((((n |^ 2) - n) / 2) * (((m |^ 2) - m) / 2))
by NEWTON:81
.=
(((n |^ 2) * (m |^ 2)) + (n * m)) / 2
.=
(((n * n) * (m |^ 2)) + (n * m)) / 2
by NEWTON:81
.=
(((n * n) * (m * m)) + (n * m)) / 2
by NEWTON:81
.=
Triangle (n * m)
by A5
;
hence
((Triangle n) * (Triangle m)) + ((Triangle (n -' 1)) * (Triangle (m -' 1))) = Triangle (n * m)
; verum