let f, g, h be Function; ( 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
; 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; verum