defpred S_{2}[ object , object ] means ex x, y being Integer st

( x > 0 & y > 0 & $1 = ((dl. 0),(dl. 1)) --> (x,y) & $2 = (dl. 0) .--> (x gcd y) );

A1: for p, q1, q2 being object st S_{2}[p,q1] & S_{2}[p,q2] holds

q1 = q2

A7: for p, q being object holds

( [p,q] in f iff ( p in FinPartSt SCM & S_{2}[p,q] ) )
from FUNCT_1:sch 1(A1);

A8: rng f c= FinPartSt SCM

take f ; :: thesis: for p, q being FinPartState of SCM holds

( [p,q] in f iff ex x, y being Integer st

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

let p, q be FinPartState of SCM; :: thesis: ( [p,q] in f iff ex x, y being Integer st

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

thus ( [p,q] in f implies ex x, y being Integer st

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) by A7; :: thesis: ( ex x, y being Integer st

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) implies [p,q] in f )

given x, y being Integer such that A10: ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ; :: thesis: [p,q] in f

p in FinPartSt SCM by MEMSTR_0:75;

hence [p,q] in f by A7, A10; :: thesis: verum

( x > 0 & y > 0 & $1 = ((dl. 0),(dl. 1)) --> (x,y) & $2 = (dl. 0) .--> (x gcd y) );

A1: for p, q1, q2 being object st S

q1 = q2

proof

consider f being Function such that
let p, q1, q2 be object ; :: thesis: ( S_{2}[p,q1] & S_{2}[p,q2] implies q1 = q2 )

given x1, y1 being Integer such that x1 > 0 and

y1 > 0 and

A2: p = ((dl. 0),(dl. 1)) --> (x1,y1) and

A3: q1 = (dl. 0) .--> (x1 gcd y1) ; :: thesis: ( not S_{2}[p,q2] or q1 = q2 )

given x2, y2 being Integer such that x2 > 0 and

y2 > 0 and

A4: p = ((dl. 0),(dl. 1)) --> (x2,y2) and

A5: q2 = (dl. 0) .--> (x2 gcd y2) ; :: thesis: q1 = q2

A6: y1 = (((dl. 0),(dl. 1)) --> (x1,y1)) . (dl. 1) by FUNCT_4:63

.= y2 by A2, A4, FUNCT_4:63 ;

x1 = (((dl. 0),(dl. 1)) --> (x1,y1)) . (dl. 0) by AMI_3:10, FUNCT_4:63

.= x2 by A2, A4, AMI_3:10, FUNCT_4:63 ;

hence q1 = q2 by A3, A5, A6; :: thesis: verum

end;given x1, y1 being Integer such that x1 > 0 and

y1 > 0 and

A2: p = ((dl. 0),(dl. 1)) --> (x1,y1) and

A3: q1 = (dl. 0) .--> (x1 gcd y1) ; :: thesis: ( not S

given x2, y2 being Integer such that x2 > 0 and

y2 > 0 and

A4: p = ((dl. 0),(dl. 1)) --> (x2,y2) and

A5: q2 = (dl. 0) .--> (x2 gcd y2) ; :: thesis: q1 = q2

A6: y1 = (((dl. 0),(dl. 1)) --> (x1,y1)) . (dl. 1) by FUNCT_4:63

.= y2 by A2, A4, FUNCT_4:63 ;

x1 = (((dl. 0),(dl. 1)) --> (x1,y1)) . (dl. 0) by AMI_3:10, FUNCT_4:63

.= x2 by A2, A4, AMI_3:10, FUNCT_4:63 ;

hence q1 = q2 by A3, A5, A6; :: thesis: verum

A7: for p, q being object holds

( [p,q] in f iff ( p in FinPartSt SCM & S

A8: rng f c= FinPartSt SCM

proof

dom f c= FinPartSt SCM
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in rng f or q in FinPartSt SCM )

assume q in rng f ; :: thesis: q in FinPartSt SCM

then consider p being object such that

A9: [p,q] in f by XTUPLE_0:def 13;

ex x, y being Integer st

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) by A7, A9;

hence q in FinPartSt SCM by MEMSTR_0:75; :: thesis: verum

end;assume q in rng f ; :: thesis: q in FinPartSt SCM

then consider p being object such that

A9: [p,q] in f by XTUPLE_0:def 13;

ex x, y being Integer st

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) by A7, A9;

hence q in FinPartSt SCM by MEMSTR_0:75; :: thesis: verum

proof

then reconsider f = f as PartFunc of (FinPartSt SCM),(FinPartSt SCM) by A8, RELSET_1:4;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in dom f or e in FinPartSt SCM )

assume e in dom f ; :: thesis: e in FinPartSt SCM

then [e,(f . e)] in f by FUNCT_1:1;

hence e in FinPartSt SCM by A7; :: thesis: verum

end;assume e in dom f ; :: thesis: e in FinPartSt SCM

then [e,(f . e)] in f by FUNCT_1:1;

hence e in FinPartSt SCM by A7; :: thesis: verum

take f ; :: thesis: for p, q being FinPartState of SCM holds

( [p,q] in f iff ex x, y being Integer st

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

let p, q be FinPartState of SCM; :: thesis: ( [p,q] in f iff ex x, y being Integer st

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

thus ( [p,q] in f implies ex x, y being Integer st

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) by A7; :: thesis: ( ex x, y being Integer st

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) implies [p,q] in f )

given x, y being Integer such that A10: ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ; :: thesis: [p,q] in f

p in FinPartSt SCM by MEMSTR_0:75;

hence [p,q] in f by A7, A10; :: thesis: verum