let S be non empty functional set ; :: thesis: dom (product" S) = meet { (dom f) where f is Element of S : verum }
set D = { (dom f) where f is Element of S : verum } ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: meet { (dom f) where f is Element of S : verum } c= dom (product" S)

let x be set ; :: thesis: ( x in dom (product" S) implies x in meet { (dom f) where f is Element of S : verum } )
assume A1: x in dom (product" S) ; :: thesis: x in meet { (dom f) where f is Element of S : verum }
set f = the Element of S;
A2: dom the Element of S in { (dom f) where f is Element of S : verum } ;
for Y being set st Y in { (dom f) where f is Element of S : verum } holds
x in Y

proof

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

end;

hence x in meet { (dom f) where f is Element of S : verum } by A2, SETFAM_1:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in meet { (dom f) where f is Element of S : verum } or x in dom (product" S) )
assume A3: x in meet { (dom f) where f is Element of S : verum } ; :: thesis: x in dom (product" S)
for f being Function st f in S holds
x in dom f

proof

let f be Function; :: thesis: ( f in S implies x in dom f )
assume f in S ; :: thesis: x in dom f
then dom f in { (dom f) where f is Element of S : verum } ;
hence x in dom f by A3, SETFAM_1:def 1; :: thesis: verum

end;

hence x in dom (product" S) by Def13; :: thesis: verum