let n be non zero Nat; :: thesis: (3 * (Triangle n)) + (Triangle (n -' 1)) = Triangle (2 * n)
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;
(3 * (Triangle n)) + (Triangle (n -' 1)) = (3 * ((n * (n + 1)) / 2)) + (((n - 1) * ((n - 1) + 1)) / 2) by A2, Th19
.= ((2 * n) * ((2 * n) + 1)) / 2
.= Triangle (2 * n) by Th19 ;
hence (3 * (Triangle n)) + (Triangle (n -' 1)) = Triangle (2 * n) ; :: thesis: verum