now :: thesis: for x being object st x in dom (the_Target_of F) holds
(the_Target_of F) . x is Function

let x be object ; :: thesis: ( x in dom (the_Target_of F) implies (the_Target_of F) . x is Function )
assume x in dom (the_Target_of F) ; :: thesis: (the_Target_of F) . x is Function
then x in dom F by Def7;
then consider G being _Graph such that
A2: ( G = F . x & (the_Target_of F) . x = the_Target_of G ) by Def7;
thus (the_Target_of F) . x is Function by A2; :: thesis: verum

end;

hence the_Target_of F is Function-yielding by FUNCOP_1:def 6; :: thesis: verum