let z1, z2 be FinSequence; :: thesis: ( len z1 = len m & ( for i being natural number st i in dom z1 holds
z1 . i = u mod (m . i) ) & len z2 = len m & ( for i being natural number st i in dom z2 holds
z2 . i = u mod (m . i) ) implies z1 = z2 )
assume A1: ( len z1 = len m & ( for i being natural number st i in dom z1 holds
z1 . i = u mod (m . i) ) ) ; :: thesis: ( not len z2 = len m or ex i being natural number st
( i in dom z2 & not z2 . i = u mod (m . i) ) or z1 = z2 )
assume A2: ( len z2 = len m & ( for i being natural number st i in dom z2 holds
z2 . i = u mod (m . i) ) ) ; :: thesis: z1 = z2
B: dom z1 = Seg (len z1) by FINSEQ_1:def 3
.= dom z2 by A1, A2, FINSEQ_1:def 3 ;

now

let x be set ; :: thesis: ( x in dom z1 implies z1 . x = z2 . x )
assume C: x in dom z1 ; :: thesis: z1 . x = z2 . x
then reconsider x' = x as Element of NAT ;
thus z1 . x = u mod (m . x') by C, A1
.= z2 . x by B, C, A2 ; :: thesis: verum

end;

hence z1 = z2 by B, FUNCT_1:9; :: thesis: verum