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