defpred S2[ 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 S2[p,q1] & S2[p,q2] holds
q1 = q2
proof
let p, q1, q2 be object ; :: thesis: ( S2[p,q1] & S2[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 S2[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;
consider f being Function such that
A7: for p, q being object holds
( [p,q] in f iff ( p in FinPartSt SCM & S2[p,q] ) ) from FUNCT_1:sch 1(A1);
 A8: rng f c= FinPartSt SCM
proof
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;
dom f c= FinPartSt SCM
proof
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;
then reconsider f = f as PartFunc of (FinPartSt SCM),(FinPartSt SCM) by A8, RELSET_1:4;
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