let a, X be set ; :: thesis: ( ( a in dom () implies () . a in a ) & dom () = X \ )
set f = ChoiceOn X;
set E = ;
set LH = dom ();
set RH = X \ ;
A1: for x being set st x in dom () holds
( x in X \ & () . x in x )
proof
let x be set ; :: thesis: ( x in dom () implies ( x in X \ & () . x in x ) )
assume x in dom () ; :: thesis: ( x in X \ & () . x in x )
then [x,(() . x)] in ChoiceOn X by FUNCT_1:def 2;
then consider x1 being Element of X \ such that
B0: ( [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: () . x in x
not x1 in by ;
then reconsider xx1 = x1 as non empty set by TARSKI:def 1;
() . 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 () implies () . a in a ) ; :: thesis: dom () = X \
for x being object st x in dom () holds
x in X \ by A1;
then A2: dom () c= X \ by TARSKI:def 3;
now :: thesis: for x being object st x in X \ holds
x in dom ()
let x be object ; :: thesis: ( x in X \ implies x in dom () )
assume AA: x in X \ ; :: thesis: x in dom ()
reconsider xx = x as set by TARSKI:1;
[x, the Element of xx] in ChoiceOn X by AA;
hence x in dom () by XTUPLE_0:def 12; :: thesis: verum
end;
then X \ c= dom () by TARSKI:def 3;
hence dom () = X \ by ; :: thesis: verum