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_{1}[ Nat] means for m1 being CR_Sequence st m1 = m | $1 holds

z1,z2 are_congruent_mod Product m1;

A28: S_{1}[ 0 ]
;

for k being Element of NAT st 0 <= k & k <= len m holds

S_{1}[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

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

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

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;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

A10: now :: thesis: for k being Element of NAT st 0 <= k & k < len m & S_{1}[k] holds

S_{1}[k + 1]

A27:
m | (len m) = m
by FINSEQ_1:58;S

let k be Element of NAT ; :: thesis: ( 0 <= k & k < len m & S_{1}[k] implies S_{1}[k + 1] )

assume that

0 <= k and

A11: k < len m ; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A12: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume that

0 <= k and

A11: k < len m ; :: thesis: ( S

assume A12: S

now :: thesis: for m1 being CR_Sequence st m1 = m | (k + 1) holds

z1,z2 are_congruent_mod Product m1

hence
Sz1,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_{1} )

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_{1}

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;

end;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 )
;

end;

suppose
k > 0
; :: thesis: z1,z2 are_congruent_mod Product b_{1}

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 Lm1;

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 by A18, Th9;

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;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 Lm1;

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 by A18, Th9;

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

suppose
k = 0
; :: thesis: z1,z2 are_congruent_mod Product b_{1}

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;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

A28: S

for k being Element of NAT st 0 <= k & k <= len m holds

S

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