let Y be Subset of X; :: thesis: Y is with_common_domain
let f, g be Function; :: according to CARD_3:def 10 :: thesis: ( f in Y & g in Y implies dom f = dom g )
thus ( f in Y & g in Y implies dom f = dom g ) by Def10; :: thesis: verum