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 RFINSEQ:33;
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, Def7;
then Sorting-Function . ((fsloc 0) .--> t) = (fsloc 0) .--> u by FUNCT_1:1;
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