let F be Function; :: thesis: ( F is g -compatible implies F is f -compatible )
assume Z: F is g -compatible ; :: thesis: F is f -compatible
let x be set ; :: according to FUNCT_1:def 20 :: thesis: ( not x in proj1 F or F . x in f . x )
assume x in dom F ; :: thesis: F . x in f . x
then X: F . x in g . x by Z, FUNCT_1:def 20;
then x in dom g by FUNCT_1:def 4;
hence F . x in f . x by X, Th8; :: thesis: verum