let n, k be Nat; :: thesis: ( n >= k implies Product ((n + 1) + (- (idseq k))) = (k !) * (n choose k) )
defpred S₁[ Nat] means ( $1 <= n implies Product ((n + 1) + (- (idseq $1))) = ($1 !) * (n choose $1) );
A1: S₁[ 0 ] by RVSUM_1:94, NEWTON:12, NEWTON:19;
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
set i1 = i + 1;
assume A3: ( S₁[i] & i + 1 <= n ) ; :: thesis: Product ((n + 1) + (- (idseq (i + 1)))) = ((i + 1) !) * (n choose (i + 1))
A4: (- 1) * <*(i + 1)*> = - <*(i + 1)*>
.= <*(- (i + 1))*> by RVSUM_1:20 ;
- (idseq (i + 1)) = (- 1) * ((idseq i) ^ <*(i + 1)*>) by FINSEQ_2:51
.= (- (idseq i)) ^ <*(- (i + 1))*> by A4, NEWTON04:43 ;
then (n + 1) + (- (idseq (i + 1))) = ((n + 1) + (- (idseq i))) ^ ((n + 1) + <*(- (i + 1))*>) by BASEL_1:3
.= ((n + 1) + (- (idseq i))) ^ <*((n + 1) + (- (i + 1)))*> by BASEL_1:2 ;
then A5: Product ((n + 1) + (- (idseq (i + 1)))) = (Product ((n + 1) + (- (idseq i)))) * ((n + 1) + (- (i + 1))) by RVSUM_1:96;
reconsider l = n - (i + 1) as Element of NAT by A3, NAT_1:21;
A6: ( i <= n & n - i = l + 1 ) by NAT_1:13, A3;
n choose (i + 1) = (n !) / (((i + 1) !) * (l !)) by A3, NEWTON:def 3;
then ((i + 1) !) * (n choose (i + 1)) = (((i + 1) !) * (n !)) / (((i + 1) !) * (l !)) by XCMPLX_1:74
.= (n !) / (l !) by XCMPLX_1:91
.= ((n !) * (l + 1)) / ((l !) * (l + 1)) by XCMPLX_1:91
.= ((n !) * (l + 1)) / ((l + 1) !) by NEWTON:15
.= (((n !) * (l + 1)) * (i !)) / (((l + 1) !) * (i !)) by XCMPLX_1:91
.= (((l + 1) * (i !)) * (n !)) / (((l + 1) !) * (i !))
.= ((l + 1) * (i !)) * ((n !) / (((l + 1) !) * (i !))) by XCMPLX_1:74
.= (((n + 1) + (- (i + 1))) * (i !)) * (n choose i) by NEWTON:def 3, A6 ;
hence Product ((n + 1) + (- (idseq (i + 1)))) = ((i + 1) !) * (n choose (i + 1)) by NAT_1:13, A3, A5; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
hence ( n >= k implies Product ((n + 1) + (- (idseq k))) = (k !) * (n choose k) ) ; :: thesis: verum