let x, y, a, b be Element of INT ; :: thesis: ( x mod a = y mod a & x mod b = y mod b & a,b are_relative_prime implies x mod (a * b) = y mod (a * b) )
assume AS: ( x mod a = y mod a & x mod b = y mod b & a,b are_relative_prime ) ; :: thesis: x mod (a * b) = y mod (a * b)
set g1 = x mod a;
set g2 = x mod b;

per cases ( a * b = 0 or a * b <> 0 ) ;

suppose C1: a * b = 0 ; :: thesis: x mod (a * b) = y mod (a * b)

thus x mod (a * b) = 0 by INT_1:def 10, C1
.= y mod (a * b) by C1, INT_1:def 10 ; :: thesis: verum

end;

suppose a * b <> 0 ; :: thesis: x mod (a * b) = y mod (a * b)

then C3: ( a <> 0 & b <> 0 ) ;
C5: y = ((y div a) * a) + (y mod a) by C3, INT_1:59;
C6: x = ((x div b) * b) + (x mod b) by C3, INT_1:59;
x - y = (((x div a) * a) + (x mod a)) - (((y div a) * a) + (y mod a)) by C3, INT_1:59, C5
.= ((x div a) - (y div a)) * a by AS ;
then a divides x - y by INT_1:def 3;
then C8: x,y are_congruent_mod a by INT_1:def 4;
x - y = (((x div b) * b) + (x mod b)) - (((y div b) * b) + (y mod b)) by C3, INT_1:59, C6
.= ((x div b) - (y div b)) * b by AS ;
then b divides x - y by INT_1:def 3;
then x,y are_congruent_mod b by INT_1:def 4;
then x,y are_congruent_mod a * b by AS, C8, INT_6:21;
then a * b divides x - y by INT_1:def 4;
then consider p being Integer such that
C11: x - y = (a * b) * p by INT_1:def 3;
reconsider I0 = 0 as Element of INT by INT_1:def 2;
thus x mod (a * b) = (y + ((a * b) * p)) mod (a * b) by C11
.= ((y mod (a * b)) + (((a * b) * p) mod (a * b))) mod (a * b) by NAT_D:66
.= ((y mod (a * b)) + ((((a * b) mod (a * b)) * (p mod (a * b))) mod (a * b))) mod (a * b) by NAT_D:67
.= ((y mod (a * b)) + ((I0 * (p mod (a * b))) mod (a * b))) mod (a * b) by INT_1:50
.= (y + I0) mod (a * b) by NAT_D:66
.= y mod (a * b) ; :: thesis: verum

end;

end;