set EE = the_subsets_of_card (n,E);
set f = { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } ;
A2:
now for x, y1, y2 being object st [x,y1] in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } & [x,y2] in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } holds
y1 = y2let x,
y1,
y2 be
object ;
( [x,y1] in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } & [x,y2] in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } implies y1 = y2 )assume
[x,y1] in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum }
;
( [x,y2] in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } implies y1 = y2 )then consider X1 being
Element of
the_subsets_of_card (
n,
E)
such that A3:
[x,y1] = [X1,((LO ^ s) .: X1)]
;
A4:
x = X1
by A3, XTUPLE_0:1;
assume
[x,y2] in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum }
;
y1 = y2then consider X2 being
Element of
the_subsets_of_card (
n,
E)
such that A5:
[x,y2] = [X2,((LO ^ s) .: X2)]
;
x = X2
by A5, XTUPLE_0:1;
hence
y1 = y2
by A3, A5, A4, XTUPLE_0:1;
verum end;
now for x being object st x in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } holds
ex y, z being object st x = [y,z]let x be
object ;
( x in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } implies ex y, z being object st x = [y,z] )assume
x in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum }
;
ex y, z being object st x = [y,z]then consider X being
Element of
the_subsets_of_card (
n,
E)
such that A6:
x = [X,((LO ^ s) .: X)]
;
reconsider y =
X,
z =
(LO ^ s) .: X as
object ;
take y =
y;
ex z being object st x = [y,z]take z =
z;
x = [y,z]thus
x = [y,z]
by A6;
verum end;
then reconsider f = { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } as Function by A2, FUNCT_1:def 1, RELAT_1:def 1;
now for x being object holds
( ( x in the_subsets_of_card (n,E) implies ex y being object st [x,y] in f ) & ( ex y being object st [x,y] in f implies x in the_subsets_of_card (n,E) ) )let x be
object ;
( ( x in the_subsets_of_card (n,E) implies ex y being object st [x,y] in f ) & ( ex y being object st [x,y] in f implies x in the_subsets_of_card (n,E) ) )given y being
object such that A7:
[x,y] in f
;
x in the_subsets_of_card (n,E)consider X being
Element of
the_subsets_of_card (
n,
E)
such that A8:
[x,y] = [X,((LO ^ s) .: X)]
by A7;
A9:
x = X
by A8, XTUPLE_0:1;
not
the_subsets_of_card (
n,
E) is
empty
by A1, Th1;
hence
x in the_subsets_of_card (
n,
E)
by A9;
verum end;
then A10:
dom f = the_subsets_of_card (n,E)
by XTUPLE_0:def 12;
now for Y being object st Y in rng f holds
Y in the_subsets_of_card (n,E)let Y be
object ;
( Y in rng f implies Y in the_subsets_of_card (n,E) )reconsider YY =
Y as
set by TARSKI:1;
assume
Y in rng f
;
Y in the_subsets_of_card (n,E)then consider X1 being
object such that A11:
[X1,Y] in f
by XTUPLE_0:def 13;
consider X2 being
Element of
the_subsets_of_card (
n,
E)
such that A12:
[X1,Y] = [X2,((LO ^ s) .: X2)]
by A11;
set fe =
(LO ^ s) | X2;
A13:
(LO ^ s) | X2 is
one-to-one
by FUNCT_1:52;
not
the_subsets_of_card (
n,
E) is
empty
by A1, Th1;
then A14:
X2 in the_subsets_of_card (
n,
E)
;
then A15:
ex
X being
Subset of
E st
(
X = X2 &
card X = n )
;
LO ^ s in Funcs (
E,
E)
by FUNCT_2:9;
then
ex
f being
Function st
(
LO ^ s = f &
dom f = E &
rng f c= E )
by FUNCT_2:def 2;
then A16:
dom ((LO ^ s) | X2) = X2
by A14, RELAT_1:62;
A17:
Y = (LO ^ s) .: X2
by A12, XTUPLE_0:1;
then
rng ((LO ^ s) | X2) = Y
by RELAT_1:115;
then
X2,
YY are_equipotent
by A13, A16;
then
card YY = n
by A15, CARD_1:5;
hence
Y in the_subsets_of_card (
n,
E)
by A17;
verum end;
then
rng f c= the_subsets_of_card (n,E)
;
then reconsider f = f as Function of (the_subsets_of_card (n,E)),(the_subsets_of_card (n,E)) by A10, FUNCT_2:2;
take
f
; for X being Element of the_subsets_of_card (n,E) holds f . X = (LO ^ s) .: X
thus
for X being Element of the_subsets_of_card (n,E) holds f . X = (LO ^ s) .: X
verumproof
let X be
Element of
the_subsets_of_card (
n,
E);
f . X = (LO ^ s) .: X
not
the_subsets_of_card (
n,
E) is
empty
by A1, Th1;
then
[X,(f . X)] in f
by A10, FUNCT_1:1;
then consider X9 being
Element of
the_subsets_of_card (
n,
E)
such that A18:
[X,(f . X)] = [X9,((LO ^ s) .: X9)]
;
X = X9
by A18, XTUPLE_0:1;
hence
f . X = (LO ^ s) .: X
by A18, XTUPLE_0:1;
verum
end;