let X be set ; :: thesis: 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; :: thesis: for P being Permutation of X st dom f = X holds
product f, product (f * P) are_equipotent
let P be Permutation of X; :: thesis: ( dom f = X implies product f, product (f * P) are_equipotent )
assume A1: dom f = X ; :: thesis: 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;

now :: thesis: for x being object st x in dom (P ") holds
f . x,(f * P) . ((P ") . x) are_equipotent

let x be object ; :: thesis: ( x in dom (P ") implies f . x,(f * P) . ((P ") . x) are_equipotent )
assume A6: x in dom (P ") ; :: thesis: f . x,(f * P) . ((P ") . x) are_equipotent
then (P ") . x in X by A4, FUNCT_1:def 3;
then (f * P) . ((P ") . x) = f . (P . ((P ") . x)) by A3, FUNCT_1:12
.= f . x by A5, A2, A6, FUNCT_1:35 ;
hence f . x,(f * P) . ((P ") . x) are_equipotent ; :: thesis: verum

end;

hence product f, product (f * P) are_equipotent by A1, A5, A4, A3, Th39; :: thesis: verum