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 ;
A3: the_subsets_of_card (n,X) <> {} by ;
then A2: x in the_subsets_of_card (n,X) ;
(f ||^ n) . x = ((.: f) | (the_subsets_of_card (n,X))) . x by
.= (.: f) . x by
.= f .: x by ;
hence (f ||^ n) . x = f .: x ; :: thesis: verum