defpred S2[ set , set ] means ex x, y being Integer st
( x > 0 & y > 0 & $1 = ((dl. 0),(dl. 1)) --> (x,y) & $2 = (dl. 0) .--> (x gcd y) );
let IT1, IT2 be PartFunc of (FinPartSt SCM),(FinPartSt SCM); :: thesis: ( ( for p, q being FinPartState of SCM holds
( [p,q] in IT1 iff ex x, y being Integer st
( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) ) & ( for p, q being FinPartState of SCM holds
( [p,q] in IT2 iff ex x, y being Integer st
( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) ) implies IT1 = IT2 )
assume that
A11: for p, q being FinPartState of SCM holds
( [p,q] in IT1 iff S2[p,q] ) and
A12: for p, q being FinPartState of SCM holds
( [p,q] in IT2 iff S2[p,q] ) ; :: thesis: IT1 = IT2
A13: for p, q being Element of FinPartSt SCM holds
( [p,q] in IT2 iff S2[p,q] )
proof
let p, q be Element of FinPartSt SCM; :: thesis: ( [p,q] in IT2 iff S2[p,q] )
thus ( [p,q] in IT2 implies S2[p,q] ) :: thesis: ( S2[p,q] implies [p,q] in IT2 )
proof
assume A14: [p,q] in IT2 ; :: thesis: S2[p,q]
reconsider p = p, q = q as FinPartState of SCM by MEMSTR_0:76;
S2[p,q] by A12, A14;
hence S2[p,q] ; :: thesis: verum
end;
thus ( S2[p,q] implies [p,q] in IT2 ) by A12; :: thesis: verum
end;
A15: for p, q being Element of FinPartSt SCM holds
( [p,q] in IT1 iff S2[p,q] )
proof
let p, q be Element of FinPartSt SCM; :: thesis: ( [p,q] in IT1 iff S2[p,q] )
thus ( [p,q] in IT1 implies S2[p,q] ) :: thesis: ( S2[p,q] implies [p,q] in IT1 )
proof
assume A16: [p,q] in IT1 ; :: thesis: S2[p,q]
reconsider p = p, q = q as FinPartState of SCM by MEMSTR_0:76;
S2[p,q] by A11, A16;
hence S2[p,q] ; :: thesis: verum
end;
thus ( S2[p,q] implies [p,q] in IT1 ) by A11; :: thesis: verum
end;
thus IT1 = IT2 from RELSET_1:sch 4(A15, A13); :: thesis: verum