let R be FinSequence of REAL ; :: thesis: ex R1 being non-increasing FinSequence of REAL st R,R1 are_fiberwise_equipotent
A1: len R = len R ;
for n being Element of NAT holds S₂[n] from NAT_1:sch 1(Lm5, Lm6);
hence ex R1 being non-increasing FinSequence of REAL st R,R1 are_fiberwise_equipotent by A1; :: thesis: verum