let n be Nat; :: thesis: (Triangle n) |^ 2 = Sum (NPower (3,n))
defpred S₁[ Nat] means (Triangle $1) |^ 2 = Sum (NPower (3,$1));
A1: S₁[ 0 ]

proof

thus (Triangle 0) |^ 2 = 0 * 0 by NEWTON:81
.= Sum (NPower (3,0)) ; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
reconsider k1 = k + 1 as Element of REAL by XREAL_0:def 1;
(Triangle (k + 1)) |^ 2 = (((k + 1) * ((k + 1) + 1)) / 2) |^ 2 by Th19
.= (((k + 1) * (k + 2)) / 2) * (((k + 1) * (k + 2)) / 2) by NEWTON:81
.= ((((k + 1) * (k + 1)) * (k + 2)) * (k + 2)) / (2 * 2)
.= ((((k + 1) |^ 2) * (k + 2)) * (k + 2)) / (2 * 2) by NEWTON:81
.= (((k + 1) |^ 2) * (((k * k) + (4 * k)) + 4)) / (2 * 2)
.= (((k + 1) |^ 2) * (((k |^ 2) + (4 * k)) + 4)) / (2 * 2) by NEWTON:81
.= (((((k + 1) |^ 2) * (k |^ 2)) / 4) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4)
.= (((((k + 1) * k) |^ 2) / (2 * 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4) by NEWTON:7
.= (((((k + 1) * k) |^ 2) / (2 |^ 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4) by NEWTON:81
.= (((((k + 1) |^ 2) * (k |^ 2)) / (2 |^ 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4) by NEWTON:7
.= (((((k + 1) * (k + 1)) * (k |^ 2)) / (2 |^ 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4) by NEWTON:81
.= (((((k + 1) * (k + 1)) * (k * k)) / (2 |^ 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4) by NEWTON:81
.= ((((((k + 1) * (k + 1)) * k) * k) / (2 * 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4) by NEWTON:81
.= (((((k + 1) * k) / 2) * (((k + 1) * k) / 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4)
.= (((Triangle k) * (((k + 1) * k) / 2)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4) by Th19
.= (((Triangle k) * (Triangle k)) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4) by Th19
.= (((Triangle k) |^ 2) + (((((k + 1) |^ 2) * 4) * k) / 4)) + ((((k + 1) |^ 2) * 4) / 4) by NEWTON:81
.= (Sum (NPower (3,k))) + (((k + 1) |^ 2) * (k + 1)) by A3
.= (Sum (NPower (3,k))) + (((k + 1) * (k + 1)) * (k + 1)) by NEWTON:81
.= (Sum (NPower (3,k))) + ((k + 1) |^ 3) by POLYEQ_3:27
.= Sum ((NPower (3,k)) ^ <*(k1 |^ 3)*>) by RVSUM_1:74
.= Sum (NPower (3,(k + 1))) by Th58 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence (Triangle n) |^ 2 = Sum (NPower (3,n)) ; :: thesis: verum