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 A2, CARD_1:66;

f in Funcs (X,Y) by A4, FUNCT_2:8;

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 A1, CARD_1:10;

then consider f2 being Function such that

A7: X c= f2 .: Y by CARD_1:66;

f1 .: X c= f1 .: (f2 .: Y) by A7, RELAT_1:123;

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 A4, GROUP_10:1;

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)) )

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 A2, CARD_1:66;

f in Funcs (X,Y) by A4, FUNCT_2:8;

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 A1, CARD_1:10;

then consider f2 being Function such that

A7: X c= f2 .: Y by CARD_1:66;

f1 .: X c= f1 .: (f2 .: Y) by A7, RELAT_1:123;

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 A4, GROUP_10:1;

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

hence
the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H))
by TARSKI:2; :: thesis: verum
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)) )

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 A18, RELAT_1:123;

( ex x9 being Subset of H st

( x9 = x & card x9 = n ) & x,f .: x are_equipotent ) by A1, A6, A18, CARD_1:33, XBOOLE_1:1;

then card X9 = n by A20, CARD_1:5;

hence y in the_subsets_of_card (n,(f .: H)) ; :: thesis: verum

end;hereby :: thesis: ( y in (f ||^ n) .: (the_subsets_of_card (n,H)) implies y in the_subsets_of_card (n,(f .: H)) )

assume
y in (f ||^ n) .: (the_subsets_of_card (n,H))
; :: thesis: 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 )

end;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

hence
y in (f ||^ n) .: (the_subsets_of_card (n,H))
by FUNCT_1:def 6; :: thesis: verum
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 A10, A9, FUNCT_1:77, XBOOLE_1:1;

then reconsider x9 = f " yy as Subset of H by A1, A10, A12, FUNCT_1:87;

f " yy,f .: (f " yy) are_equipotent by A1, A12, CARD_1:33;

then A14: card x9 = n by A11, A13, CARD_1:5;

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 A8, A15; :: 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 A10, A9, FUNCT_1:77, XBOOLE_1:1

.= (f ||^ n) . (f " yy) by A1, A2, A3, A4, A15, A16, Def2 ; :: thesis: verum

end;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 A10, A9, FUNCT_1:77, XBOOLE_1:1;

then reconsider x9 = f " yy as Subset of H by A1, A10, A12, FUNCT_1:87;

f " yy,f .: (f " yy) are_equipotent by A1, A12, CARD_1:33;

then A14: card x9 = n by A11, A13, CARD_1:5;

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 A8, A15; :: 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 A10, A9, FUNCT_1:77, XBOOLE_1:1

.= (f ||^ n) . (f " yy) by A1, A2, A3, A4, A15, A16, Def2 ; :: thesis: verum

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 A18, RELAT_1:123;

( ex x9 being Subset of H st

( x9 = x & card x9 = n ) & x,f .: x are_equipotent ) by A1, A6, A18, CARD_1:33, XBOOLE_1:1;

then card X9 = n by A20, CARD_1:5;

hence y in the_subsets_of_card (n,(f .: H)) ; :: thesis: verum