let m1, m2, a, c1, b, c2 be Integer; :: thesis: ( m1 <> 0 & m2 <> 0 & a gcd m1 divides c1 & b gcd m2 divides c2 & m1,m2 are_relative_prime implies ex w, r, s being Integer st
( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 ) )
assume A1: ( m1 <> 0 & m2 <> 0 & a gcd m1 divides c1 & b gcd m2 divides c2 & m1,m2 are_relative_prime ) ; :: thesis: ex w, r, s being Integer st
( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 )
set d1 = a gcd m1;
set d2 = b gcd m2;
A2: ( a gcd m1 <> 0 & b gcd m2 <> 0 ) by A1, INT_2:35;
A3: ( a div (a gcd m1),m1 div (a gcd m1) are_relative_prime & b div (b gcd m2),m2 div (b gcd m2) are_relative_prime ) by A1, Lm12;
then consider r being Integer such that
A4: (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 by Th15;
consider s being Integer such that
A5: (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 by A3, Th15;
A6: ( m1 = (m1 div (a gcd m1)) * (a gcd m1) & m2 = (m2 div (b gcd m2)) * (b gcd m2) ) by Lm11, INT_2:32;
then A7: ( m1 div (a gcd m1) <> 0 & m2 div (b gcd m2) <> 0 ) by A1;
A8: ( m1 div (a gcd m1) divides m1 & m2 div (b gcd m2) divides m2 ) by A6, INT_1:def 9;
A9: ( c1 = (c1 div (a gcd m1)) * (a gcd m1) & c2 = (c2 div (b gcd m2)) * (b gcd m2) ) by A1, Lm11;
A10: ( a = (a div (a gcd m1)) * (a gcd m1) & b = (b div (b gcd m2)) * (b gcd m2) ) by Lm11, INT_2:31;
A11: m1 div (a gcd m1),m2 div (b gcd m2) are_relative_prime

proof

assume not m1 div (a gcd m1),m2 div (b gcd m2) are_relative_prime ; :: thesis: contradiction
then A12: (m1 div (a gcd m1)) gcd (m2 div (b gcd m2)) <> 1 by INT_2:def 4;
reconsider e = (m1 div (a gcd m1)) gcd (m2 div (b gcd m2)) as Element of NAT by ORDINAL1:def 13;
( e divides m1 div (a gcd m1) & e divides m2 div (b gcd m2) ) by INT_2:31;
then ( e divides m1 & e divides m2 ) by A8, INT_2:13;
then e divides m1 gcd m2 by INT_2:33;
then e divides 1 by A1, INT_2:def 4;
hence contradiction by A12, WSIERP_1:20; :: thesis: verum

end;

then consider w being Integer such that
A13: (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 by Th15;
A14: for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2))

proof

let x be Integer; :: thesis: ( ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 implies x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) )
assume ( ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 ) ; :: thesis: x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2))
then ( (m1 div (a gcd m1)) * (a gcd m1) divides (((a div (a gcd m1)) * x) - (c1 div (a gcd m1))) * (a gcd m1) & (m2 div (b gcd m2)) * (b gcd m2) divides (((b div (b gcd m2)) * x) - (c2 div (b gcd m2))) * (b gcd m2) ) by A1, A6, A9, A10, Lm10;
then ( m1 div (a gcd m1) divides ((a div (a gcd m1)) * x) - (c1 div (a gcd m1)) & m2 div (b gcd m2) divides ((b div (b gcd m2)) * x) - (c2 div (b gcd m2)) ) by A2, Th7;
then ( (((a div (a gcd m1)) * x) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * x) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 ) by Lm10;
then ( r in Class (Cong (m1 div (a gcd m1))),x & s in Class (Cong (m2 div (b gcd m2))),x ) by A3, A4, A5, A7, Th26;
then ( [x,r] in Cong (m1 div (a gcd m1)) & [x,s] in Cong (m2 div (b gcd m2)) ) by EQREL_1:26;
then ( x,r are_congruent_mod m1 div (a gcd m1) & x,s are_congruent_mod m2 div (b gcd m2) ) by Def1;
then A15: ( m1 div (a gcd m1) divides x - r & m2 div (b gcd m2) divides x - s ) by INT_2:19;
m1 div (a gcd m1) divides (m1 div (a gcd m1)) * w by INT_2:12;
then A16: m1 div (a gcd m1) divides (x - r) - ((m1 div (a gcd m1)) * w) by A15, Lm4;
m2 div (b gcd m2) divides ((m1 div (a gcd m1)) * w) - (s - r) by A7, A13, Lm10;
then m2 div (b gcd m2) divides (x - s) - ((((m1 div (a gcd m1)) * w) + r) - s) by A15, Lm4;
then (m1 div (a gcd m1)) * (m2 div (b gcd m2)) divides x - (r + ((m1 div (a gcd m1)) * w)) by A11, A16, Lm13;
hence x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) by INT_2:19; :: thesis: verum

end;

take w ; :: thesis: ex r, s being Integer st
( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 )
take r ; :: thesis: ex s being Integer st
( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 )
take s ; :: thesis: ( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 )
thus ( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 ) by A4, A5, A13, A14; :: thesis: verum