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 & u is FinSequence of INT & u is non-increasing ) by Th39;
reconsider u = u as FinSequence of INT by A1;
set p = (fsloc 0 ) .--> t;
set q = (fsloc 0 ) .--> u;
[((fsloc 0 ) .--> t),((fsloc 0 ) .--> u)] in Sorting-Function by A1, 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; :: thesis: verum