let X, P 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 )
( f is one-to-one & dom f = X ) by Th67;
then ( P c= f " (f .: P) & f " (f .: P) c= P & rng f = X ) by A1, Def3, FUNCT_1:146, FUNCT_1:152;
hence ( f .: (f " P) = P & f " (f .: P) = P ) by A1, FUNCT_1:147, XBOOLE_0:def 10; :: thesis: verum