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 S1[ 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 S1[p,q] )
proof
let p, q be Element of FinPartSt SCM+FSA; :: thesis: ( [p,q] in IT1 iff S1[p,q] )
reconsider p = p, q = q as FinPartState of SCM+FSA by MEMSTR_0:76;
( [p,q] in IT1 iff S1[p,q] ) by A20;
hence ( [p,q] in IT1 iff S1[p,q] ) ; :: thesis: verum
end;
A23: for p, q being Element of FinPartSt SCM+FSA holds
( [p,q] in IT2 iff S1[p,q] )
proof
let p, q be Element of FinPartSt SCM+FSA; :: thesis: ( [p,q] in IT2 iff S1[p,q] )
reconsider p = p, q = q as FinPartState of SCM+FSA by MEMSTR_0:76;
( [p,q] in IT2 iff S1[p,q] ) by A21;
hence ( [p,q] in IT2 iff S1[p,q] ) ; :: thesis: verum
end;
thus IT1 = IT2 from RELSET_1:sch 4(A22, A23); :: thesis: verum