let n be Nat; :: thesis: for m being Nat
for F being real-valued FinSequence st m <> 0 & len F = m & ( for i, l being Nat st i in dom F & l = (n + i) - 1 holds
F . i = l choose n ) holds
Sum F = (n + m) choose (n + 1)
defpred S₁[ Nat] means for F being real-valued FinSequence st $1 <> 0 & len F = $1 & ( for i, l being Nat st i in dom F & l = (n + i) - 1 holds
F . i = l choose n ) holds
Sum F = (n + $1) choose (n + 1);
A1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: S₁[m] ; :: thesis: S₁[m + 1]
let F be real-valued FinSequence; :: thesis: ( m + 1 <> 0 & len F = m + 1 & ( for i, l being Nat st i in dom F & l = (n + i) - 1 holds
F . i = l choose n ) implies Sum F = (n + (m + 1)) choose (n + 1) )
assume that
m + 1 <> 0 and
A3: len F = m + 1 and
A4: for i, l being Nat st i in dom F & l = (n + i) - 1 holds
F . i = l choose n ; :: thesis: Sum F = (n + (m + 1)) choose (n + 1)
rng F c= REAL ;
then F is FinSequence of REAL by FINSEQ_1:def 4;
then consider G being FinSequence of REAL , x being Element of REAL such that
A5: F = G ^ <*x*> by A3, FINSEQ_2:19;
A6: m + 1 = (len G) + 1 by A3, A5, FINSEQ_2:16;

per cases ( m = 0 or m <> 0 ) ;

suppose A7: m = 0 ; :: thesis: Sum F = (n + (m + 1)) choose (n + 1)

A8: n = (n + 1) - 1 ;
reconsider c = n choose n as Element of REAL by XREAL_0:def 1;
A9: dom F = Seg 1 by A3, A7, FINSEQ_1:def 3;
then 1 in dom F ;
then F . 1 = n choose n by A4, A8;
hence Sum F = Sum <*c*> by A9, FINSEQ_1:def 8
.= n choose n by FINSOP_1:11
.= 1 by Th21
.= (n + (m + 1)) choose (n + 1) by A7, Th21 ;
:: thesis: verum

end;

suppose A10: m <> 0 ; :: thesis: Sum F = (n + (m + 1)) choose (n + 1)

A11: n + m = (n + (m + 1)) - 1 ;
A12: for i, l being Nat st i in dom G & l = (n + i) - 1 holds
G . i = l choose n

proof

A13: dom G c= dom F by A5, FINSEQ_1:26;
let i, l be Nat; :: thesis: ( i in dom G & l = (n + i) - 1 implies G . i = l choose n )
assume that
A14: i in dom G and
A15: l = (n + i) - 1 ; :: thesis: G . i = l choose n
G . i = F . i by A5, A14, FINSEQ_1:def 7;
hence G . i = l choose n by A4, A14, A15, A13; :: thesis: verum

end;

dom F = Seg (m + 1) by A3, FINSEQ_1:def 3;
then A16: (n + m) choose n = (G ^ <*x*>) . ((len G) + 1) by A4, A5, A6, A11, FINSEQ_1:4
.= x by FINSEQ_1:42 ;
thus Sum F = (Sum G) + x by A5, RVSUM_1:74
.= ((n + m) choose (n + 1)) + ((n + m) choose n) by A2, A6, A10, A12, A16
.= ((n + m) + 1) choose (n + 1) by Th22
.= (n + (m + 1)) choose (n + 1) ; :: thesis: verum

end;

end;

end;

A17: S₁[ 0 ] ;
thus for m being Nat holds S₁[m] from NAT_1:sch 2(A17, A1); :: thesis: verum