let n be Nat; :: thesis: 1 + (9 * (Triangle n)) = Triangle ((3 * n) + 1)
A1: Triangle n = (n * (n + 1)) / 2 by Th19;
Triangle ((3 * n) + 1) = (((3 * n) + 1) * (((3 * n) + 1) + 1)) / 2 by Th19
.= 1 + (9 * (Triangle n)) by A1 ;
hence 1 + (9 * (Triangle n)) = Triangle ((3 * n) + 1) ; :: thesis: verum