let z1, z2 be FinSequence of the carrier of R; :: thesis: ( len z1 = n + 1 & ( for i being Nat st i in dom z1 holds
z1 . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) ) & len z2 = n + 1 & ( for i being Nat st i in dom z2 holds
z2 . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) ) implies z1 = z2 )
assume that
A7: len z1 = n + 1 and
A8: for i being Nat st i in dom z1 holds
z1 . i = ((n choose (i -' 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i -' 1)) . y) and
A9: len z2 = n + 1 and
A10: for j being Nat st j in dom z2 holds
z2 . j = ((n choose (j -' 1)) * ((D |^ ((n + 1) -' j)) . x)) * ((D |^ (j -' 1)) . y) ; :: thesis: z1 = z2
A11: dom z1 = Seg (n + 1) by A7, FINSEQ_1:def 3
.= dom z2 by A9, FINSEQ_1:def 3 ;
for q being Nat st q in dom z1 holds
z1 . q = z2 . q

proof

let q be Nat; :: thesis: ( q in dom z1 implies z1 . q = z2 . q )
assume A12: q in dom z1 ; :: thesis: z1 . q = z2 . q
then reconsider q9 = q as Element of NAT ;
z1 . q = ((n choose (q9 -' 1)) * ((D |^ ((n + 1) -' q9)) . x)) * ((D |^ (q9 -' 1)) . y) by A8, A12
.= z2 . q9 by A10, A11, A12 ;
hence z1 . q = z2 . q ; :: thesis: verum

end;

hence z1 = z2 by A11; :: thesis: verum