defpred S_{2}[ 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 S_{2}[p,q] )
and

A12: for p, q being FinPartState of SCM holds

( [p,q] in IT2 iff S_{2}[p,q] )
; :: thesis: IT1 = IT2

A13: for p, q being Element of FinPartSt SCM holds

( [p,q] in IT2 iff S_{2}[p,q] )

( [p,q] in IT1 iff S_{2}[p,q] )

( 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 S

A12: for p, q being FinPartState of SCM holds

( [p,q] in IT2 iff S

A13: for p, q being Element of FinPartSt SCM holds

( [p,q] in IT2 iff S

proof

A15:
for p, q being Element of FinPartSt SCM holds
let p, q be Element of FinPartSt SCM; :: thesis: ( [p,q] in IT2 iff S_{2}[p,q] )

thus ( [p,q] in IT2 implies S_{2}[p,q] )
:: thesis: ( S_{2}[p,q] implies [p,q] in IT2 )_{2}[p,q] implies [p,q] in IT2 )
by A12; :: thesis: verum

end;thus ( [p,q] in IT2 implies S

proof

thus
( S
assume A14:
[p,q] in IT2
; :: thesis: S_{2}[p,q]

reconsider p = p, q = q as FinPartState of SCM by MEMSTR_0:76;

S_{2}[p,q]
by A12, A14;

hence S_{2}[p,q]
; :: thesis: verum

end;reconsider p = p, q = q as FinPartState of SCM by MEMSTR_0:76;

S

hence S

( [p,q] in IT1 iff S

proof

thus
IT1 = IT2
from RELSET_1:sch 4(A15, A13); :: thesis: verum
let p, q be Element of FinPartSt SCM; :: thesis: ( [p,q] in IT1 iff S_{2}[p,q] )

thus ( [p,q] in IT1 implies S_{2}[p,q] )
:: thesis: ( S_{2}[p,q] implies [p,q] in IT1 )_{2}[p,q] implies [p,q] in IT1 )
by A11; :: thesis: verum

end;thus ( [p,q] in IT1 implies S

proof

thus
( S
assume A16:
[p,q] in IT1
; :: thesis: S_{2}[p,q]

reconsider p = p, q = q as FinPartState of SCM by MEMSTR_0:76;

S_{2}[p,q]
by A11, A16;

hence S_{2}[p,q]
; :: thesis: verum

end;reconsider p = p, q = q as FinPartState of SCM by MEMSTR_0:76;

S

hence S