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 Z1: 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
W1: dom f = M and
W2: for x being set st x in M holds
f . x = H₁(x) from FUNCT_1:sch 3();
take f ; :: thesis: ( dom f = M & ( for X being set st X in M holds
f . X in X ) )
thus dom f = M by W1; :: 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 Z2: X in M ; :: thesis: f . X in X
then A: f . X = the Element of X by W2;
X <> {} by Z1, Z2;
hence f . X in X by A; :: thesis: verum