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