let R be real-valued FinSequence; :: thesis: ( 0 = len R implies ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent )
assume len R = 0 ; :: thesis: ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent
then reconsider a = R as real-valued non-increasing FinSequence by Th18;
reconsider a = a as non-increasing FinSequence of REAL by RVSUM_1:145;
take a ; :: thesis: R,a are_fiberwise_equipotent
thus R,a are_fiberwise_equipotent ; :: thesis: verum