defpred S2[ object , object ] means ex x, y being Integer st
( x > 0 & y > 0 & \$1 = ((),(dl. 1)) --> (x,y) & \$2 = () .--> (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. 1)) --> (x1,y1) and
A3: q1 = () .--> (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. 1)) --> (x2,y2) and
A5: q2 = () .--> (x2 gcd y2) ; :: thesis: q1 = q2
A6: y1 = (((),(dl. 1)) --> (x1,y1)) . (dl. 1) by FUNCT_4:63
.= y2 by ;
x1 = (((),(dl. 1)) --> (x1,y1)) . () by
.= x2 by ;
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 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:
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. 1)) --> (x,y) & q = () .--> (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:
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 (),() by ;
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. 1)) --> (x,y) & q = () .--> (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. 1)) --> (x,y) & q = () .--> (x gcd y) ) )

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

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