let X be functional with_common_domain set ; :: thesis: for f being Function st f in X holds
dom f = DOM X
set A = { (dom f) where f is Element of X : verum } ;
let f be Function; :: thesis: ( f in X implies dom f = DOM X )
assume Z: f in X ; :: thesis: dom f = DOM X
then dom f in { (dom f) where f is Element of X : verum } ;
then X: {(dom f)} c= { (dom f) where f is Element of X : verum } by ZFMISC_1:31;
{ (dom f) where f is Element of X : verum } c= {(dom f)}

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (dom f) where f is Element of X : verum } or e in {(dom f)} )
assume e in { (dom f) where f is Element of X : verum } ; :: thesis: e in {(dom f)}
then consider g being Element of X such that
W: e = dom g ;
e = dom f by W, Def10, Z;
hence e in {(dom f)} by TARSKI:def 1; :: thesis: verum

end;

then { (dom f) where f is Element of X : verum } = {(dom f)} by X, XBOOLE_0:def 10;
hence dom f = DOM X by SETFAM_1:10; :: thesis: verum