let f, g be real-valued FinSequence; :: thesis: ( f,g are_fiberwise_equipotent implies - f, - g are_fiberwise_equipotent )
assume A1: f,g are_fiberwise_equipotent ; :: thesis: - f, - g are_fiberwise_equipotent
then consider P being Permutation of (dom g) such that
A2: f = g * P by RFINSEQ:4;

A3: now :: thesis: ( ( len g >= 1 & - f = (- g) * P ) or ( len g < 1 & - f = (- g) * P ) )

per cases ( len g >= 1 or len g < 1 ) ;

case len g >= 1 ; :: thesis: - f = (- g) * P

hence - f = (- g) * P by A2, Th24; :: thesis: verum

end;

case len g < 1 ; :: thesis: - f = (- g) * P

then len g < 0 + 1 ;
then A4: len g = 0 by NAT_1:13;
then A5: g = {} ;
A6: len f = 0 by A1, A4, RFINSEQ:3;
then len (- f) = 0 by RVSUM_1:114;
then A7: - f = {} ;
f = {} by A6;
hence - f = (- g) * P by A2, A5, A7; :: thesis: verum

end;

end;

end;

dom (- g) = dom g by VALUED_1:8;
hence - f, - g are_fiberwise_equipotent by A3, RFINSEQ:4; :: thesis: verum