let F, G be Function; :: thesis: ( dom F = dom G implies ( F,G are_fiberwise_equipotent iff ex P being Permutation of (dom F) st F = G * P ) )
assume A1: dom F = dom G ; :: thesis: ( F,G are_fiberwise_equipotent iff ex P being Permutation of (dom F) st F = G * P )
thus ( F,G are_fiberwise_equipotent implies ex P being Permutation of (dom F) st F = G * P ) :: thesis: ( ex P being Permutation of (dom F) st F = G * P implies F,G are_fiberwise_equipotent )

proof

assume F,G are_fiberwise_equipotent ; :: thesis: ex P being Permutation of (dom F) st F = G * P
then consider I being Function such that
A2: ( dom I = dom F & rng I = dom G & I is one-to-one & F = G * I ) by Th3;
reconsider I = I as Function of (dom F),(dom F) by A1, A2, FUNCT_2:4;
reconsider I = I as Permutation of (dom F) by A1, A2, FUNCT_2:83;
take I ; :: thesis: F = G * I
thus F = G * I by A2; :: thesis: verum

end;

given P being Permutation of (dom F) such that A3: F = G * P ; :: thesis: F,G are_fiberwise_equipotent
A4: ( rng P = dom F & P is one-to-one ) by FUNCT_2:def 3;
( P is Function of (dom F),(dom F) & dom F = {} implies dom F = {} ) ;
then dom P = dom F by FUNCT_2:def 1;
hence F,G are_fiberwise_equipotent by A1, A3, A4, Th3; :: thesis: verum