let f, f1 be Function; :: thesis: dom |.{f,f1}.| = (dom f) /\ (dom f1)
consider A being non empty functional set such that
A1: A = {f,f1} and
A2: dom |.{f,f1}.| = meet { (dom x) where x is Element of A : verum } and
for i being set st i in dom |.{f,f1}.| holds
|.{f,f1}.| . 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),(dom f1)}

proof

thus { (dom x) where x is Element of A : verum } c= {(dom f),(dom f1)} :: according to XBOOLE_0:def 10 :: thesis: {(dom f),(dom f1)} 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),(dom f1)} )
assume q in { (dom x) where x is Element of A : verum } ; :: thesis: q in {(dom f),(dom f1)}
then consider x being Element of A such that
A3: q = dom x ;
( x = f or x = f1 ) by A1, TARSKI:def 2;
hence q in {(dom f),(dom f1)} by A3, TARSKI:def 2; :: thesis: verum

end;

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

end;

hence dom |.{f,f1}.| = (dom f) /\ (dom f1) by A2, SETFAM_1:11; :: thesis: verum