theorem Th28: :: WSIERP_1:28

for m, n being Integer ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)