let n be Nat; :: thesis: for X, Y being set
for f being Function of X,Y st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds
for x being Element of the_subsets_of_card (n,X) holds (f ||^ n) . x = f .: x
let X, Y be set ; :: thesis: for f being Function of X,Y st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds
for x being Element of the_subsets_of_card (n,X) holds (f ||^ n) . x = f .: x
let f be Function of X,Y; :: thesis: ( f is one-to-one & card n c= card X & not X is empty & not Y is empty implies for x being Element of the_subsets_of_card (n,X) holds (f ||^ n) . x = f .: x )
assume A1: ( f is one-to-one & card n c= card X & not X is empty & not Y is empty ) ; :: thesis: for x being Element of the_subsets_of_card (n,X) holds (f ||^ n) . x = f .: x
let x be Element of the_subsets_of_card (n,X); :: thesis: (f ||^ n) . x = f .: x
A0: dom f = X by FUNCT_2:def 1, A1;
A3: the_subsets_of_card (n,X) <> {} by A1, GROUP_10:1;
then A2: x in the_subsets_of_card (n,X) ;
(f ||^ n) . x = ((.: f) | (the_subsets_of_card (n,X))) . x by A1, Def2
.= (.: f) . x by A3, FUNCT_1:49
.= f .: x by A2, A0, FUNCT_3:def 1 ;
hence (f ||^ n) . x = f .: x ; :: thesis: verum