let G, H be FinSequence of REAL ; :: thesis: ( len G = n + 1 & ( for i, l, m being Nat st i in dom G & m = i - 1 & l = n - m holds
G . i = ((n choose m) * (a |^ l)) * (b |^ m) ) & len H = n + 1 & ( for i, l, m being Nat st i in dom H & m = i - 1 & l = n - m holds
H . i = ((n choose m) * (a |^ l)) * (b |^ m) ) implies G = H )
assume that
A7: len G = n + 1 and
A8: for i, l, m being Nat st i in dom G & m = i - 1 & l = n - m holds
G . i = ((n choose m) * (a |^ l)) * (b |^ m) ; :: thesis: ( not len H = n + 1 or ex i, l, m being Nat st
( i in dom H & m = i - 1 & l = n - m & not H . i = ((n choose m) * (a |^ l)) * (b |^ m) ) or G = H )
assume that
A9: len H = n + 1 and
A10: for i, l, m being Nat st i in dom H & m = i - 1 & l = n - m holds
H . i = ((n choose m) * (a |^ l)) * (b |^ 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 A11: i in dom G ; :: thesis: G . i = H . i
then A12: i in Seg (n + 1) by A7, 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 <= n + 1 by A12, FINSEQ_1:1;
then i - 1 <= (n + 1) - 1 by XREAL_1:9;
then reconsider l = n - m as Element of NAT by INT_1:5;
i in dom H by A9, A12, FINSEQ_1:def 3;
then H . i = ((n choose m) * (a |^ l)) * (b |^ m) by A10;
hence G . i = H . i by A8, A11; :: thesis: verum

end;

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