for s1, s2 being Real_Sequence st s1 is nonnegative & s1,s2 are_fiberwise_equipotent holds
s2 is nonnegative