let f, g be FinSequence; :: thesis: ( f,g are_fiberwise_equipotent iff ex P being Permutation of (dom g) st f = g * P )
thus ( f,g are_fiberwise_equipotent implies ex P being Permutation of (dom g) st f = g * P ) :: thesis: ( ex P being Permutation of (dom g) st f = g * P implies f,g are_fiberwise_equipotent )

proof

assume A1: f,g are_fiberwise_equipotent ; :: thesis: ex P being Permutation of (dom g) st f = g * P
then dom f = dom g by Th3;
hence ex P being Permutation of (dom g) st f = g * P by A1, CLASSES1:80; :: thesis: verum

end;

given P being Permutation of (dom g) such that A2: f = g * P ; :: thesis: f,g are_fiberwise_equipotent
( dom g = {} implies dom g = {} ) ;
then ( rng P c= dom g & dom P = dom g ) by FUNCT_2:def 1, RELAT_1:def 19;
then dom f = dom g by A2, RELAT_1:27;
hence f,g are_fiberwise_equipotent by A2, CLASSES1:80; :: thesis: verum