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

A2: 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 A1, Th108; :: thesis: verum

end;

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

then g = {} by NAT_1:14;
hence f " = (g ") * P by A1; :: thesis: verum

end;

end;

end;

dom (g ") = dom g by VALUED_1:def 7;
hence f " ,g " are_fiberwise_equipotent by A2, RFINSEQ:4; :: thesis: verum