let z1, z2 be FinSequence of the carrier of R; :: thesis: ( len z1 = m & ( for i being Nat st i in dom z1 holds
z1 . i = (((m choose (i -' 1)) + (m choose i)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) & len z2 = m & ( for i being Nat st i in dom z2 holds
z2 . i = (((m choose (i -' 1)) + (m choose i)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) implies z1 = z2 )
assume that
A7: len z1 = m and
A8: for i being Nat st i in dom z1 holds
z1 . i = (((m choose (i -' 1)) + (m choose i)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) and
A9: len z2 = m and
A10: for j being Nat st j in dom z2 holds
z2 . j = (((m choose (j -' 1)) + (m choose j)) * ((D |^ ((m + 1) -' j)) . x)) * ((D |^ j) . y) ; :: thesis: z1 = z2
A11: dom z1 = Seg m 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 . q9 = (((m choose (q9 -' 1)) + (m choose q9)) * ((D |^ ((m + 1) -' q9)) . x)) * ((D |^ q9) . 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