let a, X be set ; :: thesis: ( ( a in dom (ChoiceOn X) implies (ChoiceOn X) . a in a ) & dom (ChoiceOn X) = X \ {{}} )
set f = ChoiceOn X;
set E = {{}};
set LH = dom (ChoiceOn X);
set RH = X \ {{}};
A1: for x being set st x in dom (ChoiceOn X) holds
( x in X \ {{}} & (ChoiceOn X) . x in x )

proof

let x be set ; :: thesis: ( x in dom (ChoiceOn X) implies ( x in X \ {{}} & (ChoiceOn X) . x in x ) )
assume x in dom (ChoiceOn X) ; :: thesis: ( x in X \ {{}} & (ChoiceOn X) . x in x )
then [x,((ChoiceOn X) . x)] in ChoiceOn X by FUNCT_1:def 2;
then consider x1 being Element of X \ {{}} such that
B0: ( [x,((ChoiceOn X) . x)] = [x1, the Element of x1] & x1 in X \ {{}} ) ;
B1: x = [x1, the Element of x1] `1 by B0
.= x1 ;
hence x in X \ {{}} by B0; :: thesis: (ChoiceOn X) . x in x
not x1 in {{}} by B0, XBOOLE_0:def 5;
then reconsider xx1 = x1 as non empty set by TARSKI:def 1;
(ChoiceOn X) . x = [x1, the Element of x1] `2 by B0
.= the Element of xx1 ;
hence (ChoiceOn X) . x in x by B1; :: thesis: verum

end;

hence ( a in dom (ChoiceOn X) implies (ChoiceOn X) . a in a ) ; :: thesis: dom (ChoiceOn X) = X \ {{}}
for x being object st x in dom (ChoiceOn X) holds
x in X \ {{}} by A1;
then A2: dom (ChoiceOn X) c= X \ {{}} by TARSKI:def 3;

now :: thesis: for x being object st x in X \ {{}} holds
x in dom (ChoiceOn X)

let x be object ; :: thesis: ( x in X \ {{}} implies x in dom (ChoiceOn X) )
assume AA: x in X \ {{}} ; :: thesis: x in dom (ChoiceOn X)
reconsider xx = x as set by TARSKI:1;
[x, the Element of xx] in ChoiceOn X by AA;
hence x in dom (ChoiceOn X) by XTUPLE_0:def 12; :: thesis: verum

end;

then X \ {{}} c= dom (ChoiceOn X) by TARSKI:def 3;
hence dom (ChoiceOn X) = X \ {{}} by XBOOLE_0:def 10, A2; :: thesis: verum