let M be set ; :: thesis: ( ( for X being set st X in M holds
X <> {} ) implies ex f being Function st
( dom f = M & ( for X being set st X in M holds
f . X in X ) ) )
assume A1: for X being set st X in M holds
X <> {} ; :: thesis: ex f being Function st
( dom f = M & ( for X being set st X in M holds
f . X in X ) )
deffunc H₁( set ) -> Element of $1 = the Element of $1;
consider f being Function such that
A2: dom f = M and
A3: for X being set st X in M holds
f . X = H₁(X) from FUNCT_1:sch 5();
take f ; :: thesis: ( dom f = M & ( for X being set st X in M holds
f . X in X ) )
thus dom f = M by A2; :: thesis: for X being set st X in M holds
f . X in X
let X be set ; :: thesis: ( X in M implies f . X in X )
assume A4: X in M ; :: thesis: f . X in X
then A5: f . X = the Element of X by A3;
X <> {} by A1, A4;
hence f . X in X by A5; :: thesis: verum