let IT1, IT2 be PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA); :: thesis: ( ( for p, q being FinPartState of SCM+FSA holds
( [p,q] in IT1 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) ) & ( for p, q being FinPartState of SCM+FSA holds
( [p,q] in IT2 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) ) implies IT1 = IT2 )
assume that
A20: for p, q being FinPartState of SCM+FSA holds
( [p,q] in IT1 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) and
A21: for p, q being FinPartState of SCM+FSA holds
( [p,q] in IT2 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) ; :: thesis: IT1 = IT2
defpred S₁[ set , set ] means ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & $1 = (fsloc 0) .--> t & $2 = (fsloc 0) .--> u );
A22: for p, q being Element of FinPartSt SCM+FSA holds
( [p,q] in IT1 iff S₁[p,q] )

proof

let p, q be Element of FinPartSt SCM+FSA; :: thesis: ( [p,q] in IT1 iff S₁[p,q] )
reconsider p = p, q = q as FinPartState of SCM+FSA by MEMSTR_0:76;
( [p,q] in IT1 iff S₁[p,q] ) by A20;
hence ( [p,q] in IT1 iff S₁[p,q] ) ; :: thesis: verum

end;

A23: for p, q being Element of FinPartSt SCM+FSA holds
( [p,q] in IT2 iff S₁[p,q] )

proof

let p, q be Element of FinPartSt SCM+FSA; :: thesis: ( [p,q] in IT2 iff S₁[p,q] )
reconsider p = p, q = q as FinPartState of SCM+FSA by MEMSTR_0:76;
( [p,q] in IT2 iff S₁[p,q] ) by A21;
hence ( [p,q] in IT2 iff S₁[p,q] ) ; :: thesis: verum

end;

thus IT1 = IT2 from RELSET_1:sch 4(A22, A23); :: thesis: verum