let P, X be set ; :: thesis: for f being Permutation of X st P c= X holds
( f .: (f " P) = P & f " (f .: P) = P )
let f be Permutation of X; :: thesis: ( P c= X implies ( f .: (f " P) = P & f " (f .: P) = P ) )
assume A1: P c= X ; :: thesis: ( f .: (f " P) = P & f " (f .: P) = P )
dom f = X by Th51;
then A2: P c= f " (f .: P) by A1, FUNCT_1:76;
( f " (f .: P) c= P & rng f = X ) by Def3, FUNCT_1:82;
hence ( f .: (f " P) = P & f " (f .: P) = P ) by A1, A2, FUNCT_1:77; :: thesis: verum