let z1, z2 be FinSequence of (Polynom-Ring INT.Ring); :: thesis: ( len z1 = m & ( for i being Nat st i in dom z1 holds
z1 . i = (tau i) |^ p ) & len z2 = m & ( for i being Nat st i in dom z2 holds
z2 . i = (tau i) |^ p ) implies z1 = z2 )
assume that
A7: len z1 = m and
A8: for i being Nat st i in dom z1 holds
z1 . i = (tau i) |^ p and
A9: len z2 = m and
A10: for j being Nat st j in dom z2 holds
z2 . j = (tau j) |^ p ; :: thesis: z1 = z2
A11: dom z1 = Seg (len z1) by FINSEQ_1:def 3
.= dom z2 by A7, A9, FINSEQ_1:def 3 ;
for x being Nat st x in dom z1 holds
z1 . x = z2 . x

proof

let x be Nat; :: thesis: ( x in dom z1 implies z1 . x = z2 . x )
assume A12: x in dom z1 ; :: thesis: z1 . x = z2 . x
hence z1 . x = (tau x) |^ p by A8
.= z2 . x by A10, A11, A12 ;
:: thesis: verum

end;

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