let s1, s2 be Real_Sequence; :: thesis: ( s1 is nonnegative & s1,s2 are_fiberwise_equipotent implies s2 is nonnegative )
assume that
A1: s1 is nonnegative and
A2: s1,s2 are_fiberwise_equipotent ; :: thesis: s2 is nonnegative
consider H being Function such that
A3: ( dom H = dom s2 & rng H = dom s1 & H is one-to-one & s2 = s1 * H ) by A2, CLASSES1:77;
A4: ( dom H = NAT & rng H = NAT ) by A3, FUNCT_2:def 1;

now :: thesis: for m being Nat holds 0 <= s2 . m

let m be Nat; :: thesis: 0 <= s2 . m
A6: H . m in dom s1 by A3, A4, ORDINAL1:def 12, FUNCT_1:3;
s2 . m = s1 . (H . m) by A3, A4, ORDINAL1:def 12, FUNCT_1:13;
hence 0 <= s2 . m by A1, A6; :: thesis: verum

end;

hence s2 is nonnegative ; :: thesis: verum