let X be set ; for f being Function
for P being Permutation of X st dom f = X holds
product f, product (f * P) are_equipotent
let f be Function; for P being Permutation of X st dom f = X holds
product f, product (f * P) are_equipotent
let P be Permutation of X; ( dom f = X implies product f, product (f * P) are_equipotent )
assume A1:
dom f = X
; product f, product (f * P) are_equipotent
A2:
rng P = X
by FUNCT_2:def 3;
dom P = X
by FUNCT_2:52;
then A3:
dom (f * P) = X
by A1, A2, RELAT_1:27;
A4:
rng (P ") = X
by FUNCT_2:def 3;
A5:
dom (P ") = X
by FUNCT_2:52;
hence
product f, product (f * P) are_equipotent
by A1, A5, A4, A3, Th39; verum