let S be functional with_common_domain set ; :: thesis: dom (product" S) = DOM S

per cases ( S is empty or not S is empty ) ;

suppose A1: S is empty ; :: thesis: dom (product" S) = DOM S

hence dom (product" S) = {} by Def13, RELAT_1:60
.= DOM S by A1, Def12 ;
:: thesis: verum

end;

suppose A2: not S is empty ; :: thesis: dom (product" S) = DOM S

consider f being Element of S;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: DOM S c= dom (product" S)

let x be set ; :: thesis: ( x in dom (product" S) implies x in DOM S )
assume x in dom (product" S) ; :: thesis: x in DOM S
then x in dom f by A2, Def13;
hence x in DOM S by A2, Def12; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in DOM S or x in dom (product" S) )
assume x in DOM S ; :: thesis: x in dom (product" S)
then for f being Function st f in S holds
x in dom f by Def12;
hence x in dom (product" S) by A2, Def13; :: thesis: verum

end;

end;