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)
thus dom f = DOM S by A1, Lm2
.= dom (product" S) by Def12 ; :: thesis: verum