let G, H be FinSequence of REAL ; :: thesis: ( len G = n + 1 & ( for i, k being Nat st i in dom G & k = i - 1 holds
G . i = n choose k ) & len H = n + 1 & ( for i, k being Nat st i in dom H & k = i - 1 holds
H . i = n choose k ) implies G = H )
assume that
A5: len G = n + 1 and
A6: for i, m being Nat st i in dom G & m = i - 1 holds
G . i = n choose m ; :: thesis: ( not len H = n + 1 or ex i, k being Nat st
( i in dom H & k = i - 1 & not H . i = n choose k ) or G = H )
assume that
A7: len H = n + 1 and
A8: for i, m being Nat st i in dom H & m = i - 1 holds
H . i = n choose m ; :: thesis: G = H
for i being Nat st i in dom G holds
G . i = H . i

proof

let i be Nat; :: thesis: ( i in dom G implies G . i = H . i )
assume A9: i in dom G ; :: thesis: G . i = H . i
then A10: i in Seg (n + 1) by A5, FINSEQ_1:def 3;
then i >= 1 by FINSEQ_1:1;
then reconsider m = i - 1 as Element of NAT by INT_1:5;
i in dom H by A7, A10, FINSEQ_1:def 3;
then H . i = n choose m by A8;
hence G . i = H . i by A6, A9; :: thesis: verum

end;

hence G = H by A5, A7, FINSEQ_2:9; :: thesis: verum