let M be non empty set ; :: thesis: ( not {} in M implies for Ch being Choice_Function of M holds Ch is Function of M,(union M) )
assume A1: not {} in M ; :: thesis: for Ch being Choice_Function of M holds Ch is Function of M,(union M)
let Ch be Choice_Function of M; :: thesis: Ch is Function of M,(union M)
A2: dom Ch = M by PARTFUN1:def 2;
rng Ch c= union M

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng Ch or x in union M )
assume x in rng Ch ; :: thesis: x in union M
then consider y being object such that
A3: y in dom Ch and
A4: x = Ch . y by FUNCT_1:def 3;
reconsider y = y as set by TARSKI:1;
A5: x in y by A3, A1, A4, Lm2;
y in M by A3;
hence x in union M by A5, TARSKI:def 4; :: thesis: verum

end;

hence Ch is Function of M,(union M) by A2, FUNCT_2:2; :: thesis: verum