let n be Element of NAT ; :: thesis: (n + 2) block n = (3 * ((n + 2) choose 4)) + ((n + 2) choose 3)
defpred S₁[ Element of NAT ] means ($1 + 2) block $1 = (3 * (($1 + 2) choose 4)) + (($1 + 2) choose 3);
A1: S₁[ 0 ]

proof

( 2 choose 4 = 0 & 2 choose 3 = 0 & 2 block 0 = 0 ) by Th31, NEWTON:def 3;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
set k2 = k + 2;
set k1 = k + 1;
set k3 = (k + 2) + 1;
A4: (k + 2) block k = (3 * (((((k + 2) * ((k + 2) - 1)) * ((k + 2) - 2)) * ((k + 2) - 3)) / 24)) + ((k + 2) choose 3) by A3, Th61
.= (3 * (((((k + 2) * ((k + 2) - 1)) * ((k + 2) - 2)) * ((k + 2) - 3)) / 24)) + ((((k + 2) * ((k + 2) - 1)) * ((k + 2) - 2)) / 6) by Th61
.= ((k + 2) * ((k + 2) - 1)) * ((((3 * ((k + 2) - 2)) * ((k + 2) - 3)) / 24) + ((4 * ((k + 2) - 2)) / 24)) ;
(k + 1) * (((k + 1) + 1) block (k + 1)) = (k + 1) * ((k + 2) choose 2) by Th62
.= (k + 1) * (((k + 2) * ((k + 2) - 1)) / 2) by Th61
.= ((k + 2) * ((k + 2) - 1)) * (((k + 1) * 12) / 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, Th56
.= (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 Th61
.= (3 * (((k + 2) + 1) choose 4)) + (((k + 2) + 1) choose 3) by Th61 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2);
hence (n + 2) block n = (3 * ((n + 2) choose 4)) + ((n + 2) choose 3) ; :: thesis: verum