let g be Function; :: thesis: ( g is f -compatible implies g is X -defined )
assume g is f -compatible ; :: thesis: g is X -defined
then A1: dom g c= dom f by Th104;
dom f c= X by RELAT_1:def 18;
hence dom g c= X by A1; :: according to RELAT_1:def 18 :: thesis: verum