theorem :: WSIERP_1:34

for k, m, n, m1, n1 being Integer st m <> 0 & n <> 0 & (m * m1) + (n * n1) = k holds
for x, y being Integer st (m * x) + (n * y) = k holds
ex t being Integer st
( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) )