for F, G being Function st dom F = dom G holds
( F,G are_fiberwise_equipotent iff ex P being Permutation of (dom F) st F = G * P )