let u be INT -valued FinSequence; :: thesis: for m being CR_Sequence
for z1, z2 being Integer st 0 <= z1 & z1 < Product m & ( for i being Nat st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being Nat 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 Nat st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being Nat 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 Nat st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being Nat st i in dom m holds
z2,u . i are_congruent_mod m . i ) implies z1 = z2 )
assume that
A1: 0 <= z1 and
A2: z1 < Product m and
A3: for i being Nat st i in dom m holds
z1,u . i are_congruent_mod m . i and
A4: 0 <= z2 and
A5: z2 < Product m and
A6: for i being Nat st i in dom m holds
z2,u . i are_congruent_mod m . i ; :: thesis: z1 = z2
defpred S₁[ Nat] means for m1 being CR_Sequence st m1 = m | $1 holds
z1,z2 are_congruent_mod Product m1;

A7: now :: thesis: for i being Element of NAT st i in dom m holds
z1,z2 are_congruent_mod m . i

let i be Element of NAT ; :: thesis: ( i in dom m implies z1,z2 are_congruent_mod m . i )
assume A8: i in dom m ; :: thesis: z1,z2 are_congruent_mod m . i
then A9: u . i,z2 are_congruent_mod m . i by A6, INT_1:14;
z1,u . i are_congruent_mod m . i by A3, A8;
hence z1,z2 are_congruent_mod m . i by A9, INT_1:15; :: thesis: verum

end;

A10: now :: thesis: for k being Element of NAT st 0 <= k & k < len m & S₁[k] holds
S₁[k + 1]

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

now :: thesis: for m1 being CR_Sequence st m1 = m | (k + 1) holds
z1,z2 are_congruent_mod Product m1

set m2 = m | k;
let m1 be CR_Sequence; :: thesis: ( m1 = m | (k + 1) implies z1,z2 are_congruent_mod Product b₁ )
A13: 1 <= k + 1 by NAT_1:11;
A14: k + 1 <= len m by A11, NAT_1:13;
then k + 1 in Seg (len m) by A13;
then A15: k + 1 in dom m by FINSEQ_1:def 3;
assume A16: m1 = m | (k + 1) ; :: thesis: z1,z2 are_congruent_mod Product b₁
then A17: len m1 = k + 1 by A14, FINSEQ_1:59;
then k + 1 in Seg (len m1) by A13;
then A18: k + 1 in dom m1 by 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 A11, Th24;
set mm = (Product m1) / (m1 . (k + 1));
A19: z1,z2 are_congruent_mod Product m2 by A12;
reconsider m9 = m as FinSequence of INT by FINSEQ_1:102;
A20: m . (k + 1) = m1 . (k + 1) by A16, A18, FUNCT_1:47;
m . (k + 1) in rng m by A15, FUNCT_1:3;
then A21: m1 . (k + 1) > 0 by A20, PARTFUN3:def 1;
reconsider mm = (Product m1) / (m1 . (k + 1)) as Integer ;
A22: mm * (m1 . (k + 1)) = (Product m1) * (((m1 . (k + 1)) ") * (m1 . (k + 1)))
.= (Product m1) * 1 by A21, XCMPLX_0:def 7
.= Product m1 ;
(m9 | (k + 1)) | k = m9 | k by FINSEQ_1:82, NAT_1:11;
then m1 = m2 ^ <*(m1 . (k + 1))*> by A16, A17, FINSEQ_3:55;
then Product m1 = (Product m2) * (m1 . (k + 1)) by RVSUM_1:96;
then mm = (Product m2) * ((m1 . (k + 1)) * ((m1 . (k + 1)) ")) ;
then A23: mm = (Product m2) * 1 by A21, XCMPLX_0:def 7;
z1,z2 are_congruent_mod m1 . (k + 1) by A7, A15, A20;
hence z1,z2 are_congruent_mod Product m1 by A18, A19, A23, A22, Th21, Th25; :: thesis: verum

end;

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

then A24: m1 = <*(m1 . 1)*> by A17, FINSEQ_1:40;
then dom m1 = Seg 1 by FINSEQ_1:38;
then A25: 1 in dom m1 ;
1 <= len m by A14, A13, XXREAL_0:2;
then 1 in Seg (len m) ;
then A26: 1 in dom m by FINSEQ_1:def 3;
Product m1 = m1 . 1 by A24
.= m . 1 by A16, A25, FUNCT_1:47 ;
hence z1,z2 are_congruent_mod Product m1 by A7, A26; :: thesis: verum

end;

end;

end;

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

end;

A27: m | (len m) = m by FINSEQ_1:58;
A28: S₁[ 0 ] ;
for k being Element of NAT st 0 <= k & k <= len m holds
S₁[k] from INT_1:sch 7(A28, A10);
then A29: z1,z2 are_congruent_mod Product m by A27;
thus z1 = z1 mod (Product m) by A1, A2, NAT_D:63
.= z2 mod (Product m) by A29, NAT_D:64
.= z2 by A4, A5, NAT_D:63 ; :: thesis: verum