:: deftheorem Def10 defines with_common_domain CARD_3:def 10 :
for IT being set holds
( IT is with_common_domain iff for f, g being Function st f in IT & g in IT holds
dom f = dom g );