theorem Th25: :: INT_6:25

for m being CR_Sequence
for i being Nat st i in dom m holds
for mm being Integer st mm = (Product m) / (m . i) holds
mm,m . i are_coprime