let S be functional with_common_domain set ; :: thesis: for f being Function st f in S holds
dom f = dom (product" S)
let f be Function; :: thesis: ( f in S implies dom f = dom (product" S) )
assume A1: f in S ; :: thesis: dom f = dom (product" S)
for x being set holds
( x in dom f iff x in dom (product" S) )

proof

let x be set ; :: thesis: ( x in dom f iff x in dom (product" S) )
thus ( x in dom f implies x in dom (product" S) ) :: thesis: ( x in dom (product" S) implies x in dom f )

proof

assume x in dom f ; :: thesis: x in dom (product" S)
then for g being Function st g in S holds
x in dom g by A1, Def10;
hence x in dom (product" S) by A1, Def13; :: thesis: verum

end;

thus ( x in dom (product" S) implies x in dom f ) by A1, Def13; :: thesis: verum

end;

hence dom f = dom (product" S) by TARSKI:1; :: thesis: verum