let x be object ; :: thesis: for X being non empty functional set st ( for f being Function st f in X holds
x in dom f ) holds
x in DOM X
let X be non empty functional set ; :: thesis: ( ( for f being Function st f in X holds
x in dom f ) implies x in DOM X )
assume A1: for f being Function st f in X holds
x in dom f ; :: thesis: x in DOM X
set A = { (dom f) where f is Element of X : verum } ;
consider Y being object such that
A2: Y in X by XBOOLE_0:def 1;
reconsider Y = Y as Function by A2;
A3: dom Y in { (dom f) where f is Element of X : verum } by A2;
for Y being set st Y in { (dom f) where f is Element of X : verum } holds
x in Y

proof

let Y be set ; :: thesis: ( Y in { (dom f) where f is Element of X : verum } implies x in Y )
assume Y in { (dom f) where f is Element of X : verum } ; :: thesis: x in Y
then ex f being Element of X st Y = dom f ;
hence x in Y by A1; :: thesis: verum

end;

hence x in DOM X by A3, SETFAM_1:def 1; :: thesis: verum