let f, g be FinSequence of the carrier of R; :: thesis: ( len f = n + 1 & ( for i, l, m being Nat st i in dom f & m = i - 1 & l = n - m holds
f /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) & 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) ) implies f = g )
assume that
A4: len f = n + 1 and
A5: for i, l, m being Nat st i in dom f & m = i - 1 & l = n - m holds
f /. i = ((n choose m) * (a |^ l)) * (b |^ m) ; :: thesis: ( not len g = n + 1 or ex i, l, m being Nat st
( i in dom g & m = i - 1 & l = n - m & not g /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) or f = g )
assume that
A6: len g = n + 1 and
A7: 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: f = g
for i being Nat st 1 <= i & i <= len f holds
f . i = g . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len f implies f . i = g . i )
assume that
A8: 1 <= i and
A9: i <= len f ; :: thesis: f . i = g . i
reconsider m = i - 1 as Element of NAT by A8, INT_1:5;
i - 1 <= (n + 1) - 1 by A4, A9, XREAL_1:9;
then reconsider l = n - m as Element of NAT by INT_1:5;
A10: i in Seg (n + 1) by A4, A8, A9, FINSEQ_1:1;
then A11: i in dom f by A4, FINSEQ_1:def 3;
A12: i in dom g by A6, A10, FINSEQ_1:def 3;
hence g . i = g /. i by PARTFUN1:def 6
.= ((n choose m) * (a |^ l)) * (b |^ m) by A7, A12
.= f /. i by A5, A11
.= f . i by A11, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence f = g by A4, A6, FINSEQ_1:14; :: thesis: verum