let n be non zero Nat; :: thesis: (Triangle n) + (Triangle (n -' 1)) = (((1 + (2 * n)) - 1) * n) / 2
A1: n -' 1 = n - 1 by XREAL_1:233, NAT_1:14;
A2: Triangle (n -' 1) = ((n - 1) * ((n - 1) + 1)) / 2 by A1, Th19;
(Triangle n) + (Triangle (n -' 1)) = ((n * (n + 1)) / 2) + (Triangle (n -' 1)) by Th19
.= (((1 + (2 * n)) - 1) * n) / 2 by A2 ;
hence (Triangle n) + (Triangle (n -' 1)) = (((1 + (2 * n)) - 1) * n) / 2 ; :: thesis: verum