let p be set ; ( 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;
hereby ( ex x, y being Integer st
( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) ) implies p in dom Euclid-Function )
assume A3:
p in dom Euclid-Function
;
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) )
;
verum
end;
given x, y being Integer such that A5:
( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) )
; p in dom Euclid-Function
[p,((dl. 0) .--> (x gcd y))] in Euclid-Function
by A5, Def2;
hence
p in dom Euclid-Function
by FUNCT_1:1; verum