:: deftheorem defines with_the_same_dom ORDINAL6:def 10 :
for f being Function holds
( f is with_the_same_dom iff rng f is with_common_domain );