let t be FinSequence of INT ; :: thesis: ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing )
consider u being non-increasing FinSequence of REAL such that
A1: t,u are_fiberwise_equipotent by Th22;
take u ; :: thesis: ( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing )
thus t,u are_fiberwise_equipotent by A1; :: thesis: ( u is FinSequence of INT & u is non-increasing )
rng t = rng u by A1, CLASSES1:75;
hence u is FinSequence of INT by FINSEQ_1:def 4; :: thesis: u is non-increasing
thus u is non-increasing ; :: thesis: verum