let p be set ; :: thesis: ( p in dom Euclid-Function iff ex x, y being Integer st

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) ) )

A1: dom Euclid-Function c= FinPartSt SCM by RELAT_1:def 18;

A2: ( p in dom Euclid-Function iff [p,(Euclid-Function . p)] in Euclid-Function ) by FUNCT_1:1;

[p,((dl. 0) .--> (x gcd y))] in Euclid-Function by A5, Def2;

hence p in dom Euclid-Function by FUNCT_1:1; :: thesis: verum

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) ) )

A1: dom Euclid-Function c= FinPartSt SCM by RELAT_1:def 18;

A2: ( p in dom Euclid-Function iff [p,(Euclid-Function . p)] in Euclid-Function ) by FUNCT_1:1;

hereby :: thesis: ( ex x, y being Integer st

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) ) implies p in dom Euclid-Function )

given x, y being Integer such that A5:
( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) )
; :: thesis: p in dom Euclid-Function( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) ) implies p in dom Euclid-Function )

assume A3:
p in dom Euclid-Function
; :: thesis: ex x, y being Integer st

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) )

then Euclid-Function . p in FinPartSt SCM by PARTFUN1:4;

then A4: Euclid-Function . p is FinPartState of SCM by MEMSTR_0:76;

p is FinPartState of SCM by A1, A3, MEMSTR_0:76;

then ex x, y being Integer st

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & Euclid-Function . p = (dl. 0) .--> (x gcd y) ) by A2, A3, A4, Def2;

hence ex x, y being Integer st

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) ) ; :: thesis: verum

end;( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) )

then Euclid-Function . p in FinPartSt SCM by PARTFUN1:4;

then A4: Euclid-Function . p is FinPartState of SCM by MEMSTR_0:76;

p is FinPartState of SCM by A1, A3, MEMSTR_0:76;

then ex x, y being Integer st

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & Euclid-Function . p = (dl. 0) .--> (x gcd y) ) by A2, A3, A4, Def2;

hence ex x, y being Integer st

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) ) ; :: thesis: verum

[p,((dl. 0) .--> (x gcd y))] in Euclid-Function by A5, Def2;

hence p in dom Euclid-Function by FUNCT_1:1; :: thesis: verum