let n be Nat; :: thesis: ((Triangle n) |^ 2) + ((Triangle (n + 1)) |^ 2) = Triangle ((n + 1) |^ 2)
A1: Triangle (n + 1) = ((n + 1) * ((n + 1) + 1)) / 2 by Th19
.= ((n + 1) * (n + 2)) / 2 ;
A2: (n + 1) |^ 2 = (n + 1) * (n + 1) by NEWTON:81;
((Triangle n) |^ 2) + ((Triangle (n + 1)) |^ 2) = (((n * (n + 1)) / 2) |^ 2) + ((Triangle (n + 1)) |^ 2) by Th19
.= (((n * (n + 1)) / 2) * ((n * (n + 1)) / 2)) + ((((n + 1) * (n + 2)) / 2) |^ 2) by NEWTON:81, A1
.= (((n * (n + 1)) / 2) * ((n * (n + 1)) / 2)) + ((((n + 1) * (n + 2)) / 2) * (((n + 1) * (n + 2)) / 2)) by NEWTON:81
.= (((n + 1) |^ 2) * (((n + 1) |^ 2) + 1)) / 2 by A2
.= Triangle ((n + 1) |^ 2) by Th19 ;
hence ((Triangle n) |^ 2) + ((Triangle (n + 1)) |^ 2) = Triangle ((n + 1) |^ 2) ; :: thesis: verum