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 and
A3: rng I = dom G and
A4: I is one-to-one and
A5: F = G * I by Th77;
reconsider I = I as Function of (dom F),(dom F) by A1, A2, A3, FUNCT_2:2;
reconsider I = I as Permutation of (dom F) by A1, A3, A4, FUNCT_2:57;
take I ; :: thesis: F = G * I
thus F = G * I by A5; :: thesis: verum
end;
given P being Permutation of (dom F) such that A6: F = G * P ; :: thesis: F,G are_fiberwise_equipotent
( P is Function of (dom F),(dom F) & dom F = {} implies dom F = {} ) ;
then ( rng P = dom F & dom P = dom F ) by FUNCT_2:def 1, FUNCT_2:def 3;
hence F,G are_fiberwise_equipotent by A1, A6, Th77; :: thesis: verum