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 A1: f in X ; :: thesis: dom f = DOM X
then dom f in { (dom f) where f is Element of X : verum } ;
then A2: {(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 object ; :: 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
A3: e = dom g ;
e = dom f by A3, Def10, A1;
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 A2;
hence dom f = DOM X by SETFAM_1:10; :: thesis: verum