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

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