let x, y be Integer; :: thesis: for fp being FinSequence of NAT st ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds
fp . b > 0 ) holds
for fp1 being FinSequence of NAT st ( for b being Element of NAT st b in dom fp holds
( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) holds
x,y are_congruent_mod Product fp
let fp be FinSequence of NAT ; :: thesis: ( ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds
fp . b > 0 ) implies for fp1 being FinSequence of NAT st ( for b being Element of NAT st b in dom fp holds
( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) holds
x,y are_congruent_mod Product fp )
assume that
A1: for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 and
A2: for b being Element of NAT st b in dom fp holds
fp . b > 0 ; :: thesis: for fp1 being FinSequence of NAT st ( for b being Element of NAT st b in dom fp holds
( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) holds
x,y are_congruent_mod Product fp
let fp1 be FinSequence of NAT ; :: thesis: ( ( for b being Element of NAT st b in dom fp holds
( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) implies x,y are_congruent_mod Product fp )
assume A3: for b being Element of NAT st b in dom fp holds
( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ; :: thesis: x,y are_congruent_mod Product fp

per cases ( x >= y or x < y ) ;

suppose x >= y ; :: thesis: x,y are_congruent_mod Product fp

then x - y in NAT by INT_1:3, XREAL_1:48;
then reconsider k = x - y as Nat ;
for b being Element of NAT st b in dom fp holds
fp . b divides k

proof

let b be Element of NAT ; :: thesis: ( b in dom fp implies fp . b divides k )
assume A4: b in dom fp ; :: thesis: fp . b divides k
A5: fp . b > 0 by A2, A4;
(y - (fp1 . b)) mod (fp . b) = 0 by A3, A4;
then A6: fp . b divides y - (fp1 . b) by A5, INT_1:62;
(x - (fp1 . b)) mod (fp . b) = 0 by A3, A4;
then fp . b divides x - (fp1 . b) by A5, INT_1:62;
then fp . b divides (x - (fp1 . b)) - (y - (fp1 . b)) by A6, Lm4;
then consider i being Integer such that
A7: x - y = (fp . b) * i ;
i >= 0

proof

assume i < 0 ; :: thesis: contradiction
then k < 0 by A2, A4, A7, XREAL_1:132;
hence contradiction ; :: thesis: verum

end;

then i in NAT by INT_1:3;
then reconsider i = i as Nat ;
thus fp . b divides k by A7; :: thesis: verum

end;

then Product fp divides k by A1, Th38;
hence x,y are_congruent_mod Product fp ; :: thesis: verum

end;

suppose x < y ; :: thesis: x,y are_congruent_mod Product fp

then y - x > 0 by XREAL_1:50;
then y - x in NAT by INT_1:3;
then reconsider k = y - x as Nat ;
for b being Element of NAT st b in dom fp holds
fp . b divides k

proof

let b be Element of NAT ; :: thesis: ( b in dom fp implies fp . b divides k )
assume A8: b in dom fp ; :: thesis: fp . b divides k
A9: fp . b > 0 by A2, A8;
(y - (fp1 . b)) mod (fp . b) = 0 by A3, A8;
then A10: fp . b divides y - (fp1 . b) by A9, INT_1:62;
(x - (fp1 . b)) mod (fp . b) = 0 by A3, A8;
then fp . b divides x - (fp1 . b) by A9, INT_1:62;
then fp . b divides (y - (fp1 . b)) - (x - (fp1 . b)) by A10, Lm4;
then consider i being Integer such that
A11: y - x = (fp . b) * i ;
k = (fp . b) * i by A11;
then i >= 0 by A2, A8, XREAL_1:132;
then i in NAT by INT_1:3;
then reconsider i = i as Nat ;
thus fp . b divides k by A11; :: thesis: verum

end;

then Product fp divides k by A1, Th38;
then y,x are_congruent_mod Product fp ;
hence x,y are_congruent_mod Product fp by INT_1:14; :: thesis: verum

end;

end;