let a, X be set ; :: thesis:
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 )

let x be set ; :: thesis:
assume x in dom (ChoiceOn X) ; :: thesis:
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:
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:

end;

end;