let i, j be Integer; :: thesis: ( i > 0 & j > 0 implies Euclid-Function . (((dl. 0),(dl. 1)) --> (i,j)) = (dl. 0) .--> (i gcd j) )
assume ( i > 0 & j > 0 ) ; :: thesis: Euclid-Function . (((dl. 0),(dl. 1)) --> (i,j)) = (dl. 0) .--> (i gcd j)
then [(((dl. 0),(dl. 1)) --> (i,j)),((dl. 0) .--> (i gcd j))] in Euclid-Function by Def2;
hence Euclid-Function . (((dl. 0),(dl. 1)) --> (i,j)) = (dl. 0) .--> (i gcd j) by FUNCT_1:1; :: thesis: verum