let X be set ; :: thesis: for f being Function st X <> {} & X c= dom f holds
f .: X <> {}
let f be Function; :: thesis: ( X <> {} & X c= dom f implies f .: X <> {} )
assume X <> {} ; :: thesis: ( not X c= dom f or f .: X <> {} )
then ex x being object st x in X by XBOOLE_0:def 1;
hence ( not X c= dom f or f .: X <> {} ) by Th107; :: thesis: verum