let f, g, h be Function; :: thesis: ( dom f = dom g & rng f c= dom h & rng g c= dom h & f,g are_fiberwise_equipotent implies h * f,h * g are_fiberwise_equipotent )
assume that
A1: dom f = dom g and
A2: rng f c= dom h and
A3: rng g c= dom h and
A4: f,g are_fiberwise_equipotent ; :: thesis: h * f,h * g are_fiberwise_equipotent
consider p being Permutation of (dom f) such that
A5: f = g * p by A1, A4, Th80;
A6: dom (h * f) = dom f by A2, RELAT_1:27;
A7: dom (h * g) = dom g by A3, RELAT_1:27;
h * f = (h * g) * p by A5, RELAT_1:36;
hence h * f,h * g are_fiberwise_equipotent by A1, A6, A7, Th80; :: thesis: verum