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