let i, j be Integer; :: thesis: ( i > 0 & j > 0 implies Euclide-Function . ((dl. 0 ),(dl. 1) --> i,j) = (dl. 0 ) .--> (i gcd j) )
assume ( i > 0 & j > 0 ) ; :: thesis: Euclide-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 Euclide-Function by Def2;
hence Euclide-Function . ((dl. 0 ),(dl. 1) --> i,j) = (dl. 0 ) .--> (i gcd j) by FUNCT_1:8; :: thesis: verum