A4: dom |.f.| = dom f by Def11;
thus dom |.f.| c= X by A4; :: according to RELAT_1:def 18 :: thesis: verum