let t be FinSequence of INT ; :: thesis: ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & Sorting-Function . ((fsloc 0 ) .--> t) = (fsloc 0 ) .--> u )
consider u being FinSequence of REAL such that
A1: t,u are_fiberwise_equipotent and
A2: u is FinSequence of INT and
A3: u is non-increasing by Th39;
reconsider u = u as FinSequence of INT by A2;
set p = (fsloc 0 ) .--> t;
set q = (fsloc 0 ) .--> u;
[((fsloc 0 ) .--> t),((fsloc 0 ) .--> u)] in Sorting-Function by A1, A3, Def3;
then Sorting-Function . ((fsloc 0 ) .--> t) = (fsloc 0 ) .--> u by FUNCT_1:8;
hence ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & Sorting-Function . ((fsloc 0 ) .--> t) = (fsloc 0 ) .--> u ) by A1, A3; :: thesis: verum