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 )

t is FinSequence of REAL by FINSEQ_3:117;

then 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

( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing )

t is FinSequence of REAL by FINSEQ_3:117;

then 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