let n be Nat; :: thesis: (n + 2) block n = (3 * ((n + 2) choose 4)) + ((n + 2) choose 3)
defpred S₁[ Nat] means ($1 + 2) block $1 = (3 * (($1 + 2) choose 4)) + (($1 + 2) choose 3);
A1: 2 choose 3 = 0 by NEWTON:def 3;
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]
set k1 = k + 1;
set k2 = k + 2;
set k3 = (k + 2) + 1;
A4: (k + 1) * (((k + 1) + 1) block (k + 1)) = (k + 1) * ((k + 2) choose 2) by Th52
.= (k + 1) * (((k + 2) * ((k + 2) - 1)) / 2) by Th51
.= ((k + 2) * ((k + 2) - 1)) * (((k + 1) * 12) / 24) ;
(k + 2) block k = (3 * (((((k + 2) * ((k + 2) - 1)) * ((k + 2) - 2)) * ((k + 2) - 3)) / 24)) + ((k + 2) choose 3) by A3, Th51
.= (3 * (((((k + 2) * ((k + 2) - 1)) * ((k + 2) - 2)) * ((k + 2) - 3)) / 24)) + ((((k + 2) * ((k + 2) - 1)) * ((k + 2) - 2)) / 6) by Th51
.= ((k + 2) * ((k + 2) - 1)) * ((((3 * ((k + 2) - 2)) * ((k + 2) - 3)) / 24) + ((4 * ((k + 2) - 2)) / 24)) ;
then ((k + 2) + 1) block (k + 1) = (((k + 2) * (k + 1)) * (((k + 1) * 12) / 24)) + (((k + 2) * (k + 1)) * ((((3 * k) * ((k + 2) - 3)) / 24) + ((4 * k) / 24))) by A4, Th46
.= (3 * ((((((k + 2) + 1) * (((k + 2) + 1) - 1)) * (((k + 2) + 1) - 2)) * (((k + 2) + 1) - 3)) / 24)) + (((((k + 2) + 1) * (k + 2)) * (k + 1)) / 6)
.= (3 * (((k + 2) + 1) choose 4)) + (((((k + 2) + 1) * (((k + 2) + 1) - 1)) * (((k + 2) + 1) - 2)) / 6) by Th51
.= (3 * (((k + 2) + 1) choose 4)) + (((k + 2) + 1) choose 3) by Th51 ;
hence S₁[k + 1] ; :: thesis: verum

end;

2 choose 4 = 0 by NEWTON:def 3;
then A5: S₁[ 0 ] by A1, Th31;
for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A2);
hence (n + 2) block n = (3 * ((n + 2) choose 4)) + ((n + 2) choose 3) ; :: thesis: verum