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

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

end;

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