let f, g be Function; :: thesis: ( f is g -compatible & dom f = dom g implies g is non-empty )
assume A1: ( f is g -compatible & dom f = dom g ) ; :: thesis: g is non-empty
let x be set ; :: according to FUNCT_1:def 9 :: thesis: ( x in dom g implies not g . x is empty )
assume x in dom g ; :: thesis: not g . x is empty
hence not g . x is empty by A1, Def20; :: thesis: verum