let p be set ; :: thesis: ( p in dom Euclide-Function iff ex x, y being Integer st
( x > 0 & y > 0 & p = (dl. 0 ),(dl. 1) --> x,y ) )
A1: ( p in dom Euclide-Function iff [p,(Euclide-Function . p)] in Euclide-Function ) by FUNCT_1:8;
A2: dom Euclide-Function c= FinPartSt SCM by RELAT_1:def 18;

hereby :: thesis: ( ex x, y being Integer st
( x > 0 & y > 0 & p = (dl. 0 ),(dl. 1) --> x,y ) implies p in dom Euclide-Function )

assume A3: p in dom Euclide-Function ; :: thesis: ex x, y being Integer st
( x > 0 & y > 0 & p = (dl. 0 ),(dl. 1) --> x,y )
then ( p in FinPartSt SCM & Euclide-Function . p in FinPartSt SCM ) by A2, PARTFUN1:27;
then ( p is FinPartState of SCM & Euclide-Function . p is FinPartState of SCM ) by AMI_1:125;
then ex x, y being Integer st
( x > 0 & y > 0 & p = (dl. 0 ),(dl. 1) --> x,y & Euclide-Function . p = (dl. 0 ) .--> (x gcd y) ) by A1, A3, Def2;
hence ex x, y being Integer st
( x > 0 & y > 0 & p = (dl. 0 ),(dl. 1) --> x,y ) ; :: thesis: verum

end;

given x, y being Integer such that A4: ( x > 0 & y > 0 & p = (dl. 0 ),(dl. 1) --> x,y ) ; :: thesis: p in dom Euclide-Function
[p,((dl. 0 ) .--> (x gcd y))] in Euclide-Function by A4, Def2;
hence p in dom Euclide-Function by FUNCT_1:8; :: thesis: verum