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

let x, y1, y2 be set ; :: 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, ZFMISC_1:33;
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, ZFMISC_1:33;
hence y1 = y2 by A3, A5, A4, ZFMISC_1:33; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card n,E : verum } implies ex y, z being set 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 set 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 set ;
take y = y; :: thesis: ex z being set 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

let x be set ; :: thesis: ( ( x in the_subsets_of_card n,E implies ex y being set st [x,y] in f ) & ( ex y being set st [x,y] in f implies x in the_subsets_of_card n,E ) )

hereby :: thesis: ( ex y being set 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 set st [x,y] in f
then reconsider X = x as Element of the_subsets_of_card n,E ;
reconsider y = (LO ^ s) .: X as set ;
take y = y; :: thesis: [x,y] in f
thus [x,y] in f ; :: thesis: verum

end;

given y being set 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, ZFMISC_1:33;
not the_subsets_of_card n,E is empty by A1, Th2;
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 RELAT_1:def 4;

now

let Y be set ; :: thesis: ( Y in rng f implies Y in the_subsets_of_card n,E )
assume Y in rng f ; :: thesis: Y in the_subsets_of_card n,E
then consider X1 being set such that
A11: [X1,Y] in f by RELAT_1:def 5;
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;
LO ^ s is one-to-one by Th1;
then A13: (LO ^ s) | X2 is one-to-one by FUNCT_1:84;
not the_subsets_of_card n,E is empty by A1, Th2;
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:12;
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:91;
A17: Y = (LO ^ s) .: X2 by A12, ZFMISC_1:33;
then rng ((LO ^ s) | X2) = Y by RELAT_1:148;
then X2,Y are_equipotent by A13, A16, WELLORD2:def 4;
then card Y = n by A15, CARD_1:21;
hence Y in the_subsets_of_card n,E by A17; :: thesis: verum

end;

then rng f c= the_subsets_of_card n,E by TARSKI:def 3;
then reconsider f = f as Function of (the_subsets_of_card n,E),(the_subsets_of_card n,E) by A10, FUNCT_2:4;
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, Th2;
then [X,(f . X)] in f by A10, FUNCT_1:8;
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, ZFMISC_1:33;
hence f . X = (LO ^ s) .: X by A18, ZFMISC_1:33; :: thesis: verum

end;