let z1, z2 be FinSequence of the carrier of R; :: thesis: ( len z1 = len s & ( for i being Nat st i in dom z1 holds
z1 . i = Product (Replace (s,i,(D . (s /. i)))) ) & len z2 = len s & ( for i being Nat st i in dom z2 holds
z2 . i = Product (Replace (s,i,(D . (s /. i)))) ) implies z1 = z2 )
assume that
A7: len z1 = len s and
A8: for i being Nat st i in dom z1 holds
z1 . i = Product (Replace (s,i,(D . (s /. i)))) and
A9: len z2 = len s and
A10: for j being Nat st j in dom z2 holds
z2 . j = Product (Replace (s,j,(D . (s /. j)))) ; :: thesis: z1 = z2
A11: dom z1 = Seg (len s) 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 = Product (Replace (s,q9,(D . (s /. q9)))) by A8, A12
.= z2 . q9 by A10, A11, A12 ;
hence z1 . q = z2 . q ; :: thesis: verum

end;

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