let Y be Subset of ; :: 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 )
assume ( f in Y & g in Y ) ; :: thesis: dom f = dom g
then ( f in X & g in X ) ;
hence dom f = dom g by Def10; :: thesis: verum