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 )

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;

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

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

hence
( a in dom (ChoiceOn X) implies (ChoiceOn X) . a in a )
; :: thesis: dom (ChoiceOn X) = X \ {{}}
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;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

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)

then
X \ {{}} c= dom (ChoiceOn X)
by TARSKI:def 3;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;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

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