let F be Function; :: thesis: ( F is g -compatible implies F is f -compatible )
assume A1: F is g -compatible ; :: thesis: F is f -compatible
let x be object ; :: according to FUNCT_1:def 14 :: thesis: ( not x in proj1 F or F . x in f . x )
assume x in dom F ; :: thesis: F . x in f . x
then A2: F . x in g . x by A1;
then x in dom g by FUNCT_1:def 2;
hence F . x in f . x by A2, Th2; :: thesis: verum