theorem :: INT_4:39

for x, y being Integer
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