let u be integer-yielding FinSequence; :: thesis: for m being CR_Sequence
for z1, z2 being Integer st 0 <= z1 & z1 < Product m & ( for i being natural number st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being natural number st i in dom m holds
z2,u . i are_congruent_mod m . i ) holds
z1 = z2
let m be CR_Sequence; :: thesis: for z1, z2 being Integer st 0 <= z1 & z1 < Product m & ( for i being natural number st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being natural number st i in dom m holds
z2,u . i are_congruent_mod m . i ) holds
z1 = z2
let z1, z2 be Integer; :: thesis: ( 0 <= z1 & z1 < Product m & ( for i being natural number st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being natural number st i in dom m holds
z2,u . i are_congruent_mod m . i ) implies z1 = z2 )
assume AS2: ( 0 <= z1 & z1 < Product m & ( for i being natural number st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being natural number st i in dom m holds
z2,u . i are_congruent_mod m . i ) ) ; :: thesis: z1 = z2

H: now

let i be Element of NAT ; :: thesis: ( i in dom m implies z1,z2 are_congruent_mod m . i )
assume i in dom m ; :: thesis: z1,z2 are_congruent_mod m . i
then ( z1,u . i are_congruent_mod m . i & z2,u . i are_congruent_mod m . i ) by AS2;
then ( z1,u . i are_congruent_mod m . i & u . i,z2 are_congruent_mod m . i ) by INT_1:35;
hence z1,z2 are_congruent_mod m . i by INT_1:36; :: thesis: verum

end;

defpred S₁[ Nat] means for m1 being CR_Sequence st m1 = m | $1 holds
z1,z2 are_congruent_mod Product m1;
A: S₁[ 0 ] ;

B: now

let k be Element of NAT ; :: thesis: ( 0 <= k & k < len m & S₁[k] implies S₁[k + 1] )
assume B0: ( 0 <= k & k < len m ) ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: S₁[k] ; :: thesis: S₁[k + 1]

now

let m1 be CR_Sequence; :: thesis: ( m1 = m | (k + 1) implies z1,z2 are_congruent_mod Product b₁ )
assume C0: m1 = m | (k + 1) ; :: thesis: z1,z2 are_congruent_mod Product b₁
set m2 = m | k;
C7: k + 1 <= len m by B0, NAT_1:13;
then C6: len m1 = k + 1 by C0, FINSEQ_1:80;
C5: 1 <= k + 1 by NAT_1:11;
then C8: ( k + 1 in Seg (len m1) & k + 1 in Seg (len m) ) by C6, C7;
C1: ( k + 1 in dom m1 & k + 1 in dom m ) by C8, FINSEQ_1:def 3;

per cases ( k > 0 or k = 0 ) ;

suppose k > 0 ; :: thesis: z1,z2 are_congruent_mod Product b₁

then reconsider m2 = m | k as CR_Sequence by B0, CRsub;
B2: z1,z2 are_congruent_mod Product m2 by B1;
B5: m . (k + 1) = m1 . (k + 1) by C1, C0, FUNCT_1:70;
m . (k + 1) in rng m by C1, FUNCT_1:12;
then B4: m1 . (k + 1) > 0 by B5, PARTFUN3:def 1;
set mm = (Product m1) / (m1 . (k + 1));
reconsider mm = (Product m1) / (m1 . (k + 1)) as Integer by prodint, C1;
reconsider m' = m as FinSequence of INT by intint;
(m' | (k + 1)) | k = m' | k by FINSEQ_1:103, NAT_1:11;
then m1 = m2 ^ <*(m1 . (k + 1))*> by C0, C6, FINSEQ_3:61;
then Product m1 = (Product m2) * (m1 . (k + 1)) by RVSUM_1:126;
then mm = (Product m2) * ((m1 . (k + 1)) * ((m1 . (k + 1)) " )) ;
then C3: mm = (Product m2) * 1 by B4, XCMPLX_0:def 7;
B3: z1,z2 are_congruent_mod m1 . (k + 1) by B5, C1, H;
mm * (m1 . (k + 1)) = (Product m1) * (((m1 . (k + 1)) " ) * (m1 . (k + 1)))
.= (Product m1) * 1 by B4, XCMPLX_0:def 7
.= Product m1 ;
hence z1,z2 are_congruent_mod Product m1 by B3, C3, B2, x1a, C1, prodgcd; :: thesis: verum

end;

suppose k = 0 ; :: thesis: z1,z2 are_congruent_mod Product b₁

then C1: m1 = <*(m1 . 1)*> by C6, FINSEQ_1:57;
then dom m1 = Seg 1 by FINSEQ_1:55;
then C4: 1 in dom m1 ;
1 <= len m by C5, C7, XXREAL_0:2;
then 1 in Seg (len m) ;
then C5: 1 in dom m by FINSEQ_1:def 3;
Product m1 = m1 . 1 by C1, RVSUM_1:125
.= m . 1 by C4, C0, FUNCT_1:70 ;
hence z1,z2 are_congruent_mod Product m1 by C5, H; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Element of NAT st 0 <= k & k <= len m holds
S₁[k] from POLYNOM2:sch 4(A, B);
m | (len m) = m by FINSEQ_1:79;
then A: z1,z2 are_congruent_mod Product m by I;
thus z1 = z1 mod (Product m) by AS2, INT_3:10
.= z2 mod (Product m) by A, INT_3:12
.= z2 by AS2, INT_3:10 ; :: thesis: verum