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 :: thesis: 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 = y2

let x, y1, y2 be object ; :: thesis: ( [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 } ; :: thesis: ( [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 } ; :: thesis: y1 = y2
then 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; :: thesis: verum

end;

now :: thesis: 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 ; :: thesis: ( 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 } ; :: thesis: 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; :: thesis: ex z being object st x = [y,z]
take z = z; :: thesis: x = [y,z]
thus x = [y,z] by A6; :: thesis: 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 :: thesis: 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 ; :: thesis: ( ( 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) ) )

hereby :: thesis: ( ex y being object st [x,y] in f implies x in the_subsets_of_card (n,E) )

assume x in the_subsets_of_card (n,E) ; :: thesis: ex y being object st [x,y] in f
then reconsider X = x as Element of the_subsets_of_card (n,E) ;
reconsider y = (LO ^ s) .: X as object ;
take y = y; :: thesis: [x,y] in f
thus [x,y] in f ; :: thesis: verum

end;

given y being object such that A7: [x,y] in f ; :: thesis: 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; :: thesis: verum

end;

then A10: dom f = the_subsets_of_card (n,E) by XTUPLE_0:def 12;

now :: thesis: for Y being object st Y in rng f holds
Y in the_subsets_of_card (n,E)

let Y be object ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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 :: thesis: verum

proof

let X be Element of the_subsets_of_card (n,E); :: thesis: 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; :: thesis: verum

end;