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