let R be FinSequence of REAL ; :: 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 non-increasing FinSequence of REAL by Th18;
take a ; :: thesis: R,a are_fiberwise_equipotent
thus R,a are_fiberwise_equipotent ; :: thesis: verum