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
A9: 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
A10: 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 );
A11: 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 AMI_1:125;
( [p,q] in IT1 iff S₁[p,q] ) by A9;
hence ( [p,q] in IT1 iff S₁[p,q] ) ; :: thesis: verum

end;

A12: 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 AMI_1:125;
( [p,q] in IT2 iff S₁[p,q] ) by A10;
hence ( [p,q] in IT2 iff S₁[p,q] ) ; :: thesis: verum

end;

thus IT1 = IT2 from RELSET_1:sch 4(A11, A12); :: thesis: verum