dom (Objs F) = dom F by Def2
.= A by PARTFUN1:def 4 ;
hence Objs F is A -defined by RELAT_1:def 18; :: thesis: verum