let n be Nat; :: thesis: for X, Y being set
for f being Function of X,Y
for H being Subset of X st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds
the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H))

let X, Y be set ; :: thesis: for f being Function of X,Y
for H being Subset of X st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds
the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H))

let f be Function of X,Y; :: thesis: for H being Subset of X st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds
the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H))

let H be Subset of X; :: thesis: ( f is one-to-one & card n c= card X & not X is empty & not Y is empty implies the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H)) )
assume that
A1: f is one-to-one and
A2: card n c= card X and
A3: not X is empty and
A4: not Y is empty ; :: thesis: the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H))
consider f1 being Function such that
A5: n c= f1 .: X by ;
f in Funcs (X,Y) by ;
then A6: ex f9 being Function st
( f = f9 & dom f9 = X & rng f9 c= Y ) by FUNCT_2:def 2;
then card X c= card Y by ;
then consider f2 being Function such that
A7: X c= f2 .: Y by CARD_1:66;
f1 .: X c= f1 .: (f2 .: Y) by ;
then n c= f1 .: (f2 .: Y) by A5;
then n c= (f1 * f2) .: Y by RELAT_1:126;
then card n c= card Y by CARD_1:66;
then not the_subsets_of_card (n,Y) is empty by ;
then f ||^ n in Funcs ((the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y))) by FUNCT_2:8;
then A8: ex fn being Function st
( f ||^ n = fn & dom fn = the_subsets_of_card (n,X) & rng fn c= the_subsets_of_card (n,Y) ) by FUNCT_2:def 2;
for y being object holds
( y in the_subsets_of_card (n,(f .: H)) iff y in (f ||^ n) .: (the_subsets_of_card (n,H)) )
proof
let y be object ; :: thesis: ( y in the_subsets_of_card (n,(f .: H)) iff y in (f ||^ n) .: (the_subsets_of_card (n,H)) )
hereby :: thesis: ( y in (f ||^ n) .: (the_subsets_of_card (n,H)) implies y in the_subsets_of_card (n,(f .: H)) )
A9: f .: H c= rng f by RELAT_1:111;
assume A10: y in the_subsets_of_card (n,(f .: H)) ; :: thesis: y in (f ||^ n) .: (the_subsets_of_card (n,H))
then A11: ex X9 being Subset of (f .: H) st
( y = X9 & card X9 = n ) ;
ex x being set st
( x in dom (f ||^ n) & x in the_subsets_of_card (n,H) & y = (f ||^ n) . x )
proof
reconsider yy = y as set by TARSKI:1;
set x = f " yy;
take f " yy ; :: thesis: ( f " yy in dom (f ||^ n) & f " yy in the_subsets_of_card (n,H) & y = (f ||^ n) . (f " yy) )
A12: f " yy c= dom f by RELAT_1:132;
A13: f .: (f " yy) = y by ;
then reconsider x9 = f " yy as Subset of H by ;
f " yy,f .: (f " yy) are_equipotent by ;
then A14: card x9 = n by ;
then A15: f " yy in the_subsets_of_card (n,H) ;
A16: the_subsets_of_card (n,H) c= the_subsets_of_card (n,X) by Lm1;
hence f " yy in dom (f ||^ n) by ; :: thesis: ( f " yy in the_subsets_of_card (n,H) & y = (f ||^ n) . (f " yy) )
thus f " yy in the_subsets_of_card (n,H) by A14; :: thesis: y = (f ||^ n) . (f " yy)
thus y = f .: (f " yy) by
.= (f ||^ n) . (f " yy) by A1, A2, A3, A4, A15, A16, Def2 ; :: thesis: verum
end;
hence y in (f ||^ n) .: (the_subsets_of_card (n,H)) by FUNCT_1:def 6; :: thesis: verum
end;
assume y in (f ||^ n) .: (the_subsets_of_card (n,H)) ; :: thesis: y in the_subsets_of_card (n,(f .: H))
then consider x being object such that
A17: x in dom (f ||^ n) and
A18: x in the_subsets_of_card (n,H) and
A19: y = (f ||^ n) . x by FUNCT_1:def 6;
reconsider x = x as Element of the_subsets_of_card (n,X) by A17;
A20: y = f .: x by A1, A2, A3, A4, A19, Def2;
then reconsider X9 = y as Subset of (f .: H) by ;
( ex x9 being Subset of H st
( x9 = x & card x9 = n ) & x,f .: x are_equipotent ) by ;
then card X9 = n by ;
hence y in the_subsets_of_card (n,(f .: H)) ; :: thesis: verum
end;
hence the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H)) by TARSKI:2; :: thesis: verum