let f be Function; :: thesis: dom |.{f}.| = dom f
consider A being non empty functional set such that
A1: A = {f} and
A2: dom |.{f}.| = meet { (dom x) where x is Element of A : verum } and
for i being set st i in dom |.{f}.| holds
|.{f}.| . i = { (x . i) where x is Element of A : verum } by Def2;
set m = { (dom x) where x is Element of A : verum } ;
{ (dom x) where x is Element of A : verum } = {(dom f)}

proof

thus { (dom x) where x is Element of A : verum } c= {(dom f)} :: according to XBOOLE_0:def 10 :: thesis: {(dom f)} c= { (dom x) where x is Element of A : verum }

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (dom x) where x is Element of A : verum } or q in {(dom f)} )
assume q in { (dom x) where x is Element of A : verum } ; :: thesis: q in {(dom f)}
then consider x being Element of A such that
A3: q = dom x ;
x = f by A1, TARSKI:def 1;
hence q in {(dom f)} by A3, TARSKI:def 1; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {(dom f)} or q in { (dom x) where x is Element of A : verum } )
assume q in {(dom f)} ; :: thesis: q in { (dom x) where x is Element of A : verum }
then A4: q = dom f by TARSKI:def 1;
f is Element of A by A1, TARSKI:def 1;
hence q in { (dom x) where x is Element of A : verum } by A4; :: thesis: verum

end;

hence dom |.{f}.| = dom f by A2, SETFAM_1:10; :: thesis: verum