theorem Th9: :: AMI_4:9

for i, j being Integer st i > 0 & j > 0 holds
Euclid-Function . (((dl. 0),(dl. 1)) --> (i,j)) = (dl. 0) .--> (i gcd j)