let f be Function; :: thesis: for g being f -compatible Function holds dom g c= dom f
let g be f -compatible Function; :: thesis: dom g c= dom f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom g or x in dom f )
assume x in dom g ; :: thesis: x in dom f
then g . x in f . x by Def14;
hence x in dom f by Def2; :: thesis: verum