let f be Function; :: thesis:

hereby :: thesis:

assume A10: f = the_Target_of F ; :: thesis:
hence dom f = dom F by Def7; :: thesis:
let x be Element of dom F; :: thesis:
consider G being _Graph such that
A11: ( G = F . x & f . x = the_Target_of G ) by A10, Def7;
thus f . x = the_Target_of (F . x) by A11; :: thesis:

end;

assume A12: ( dom f = dom F & ( for x being Element of dom F holds f . x = the_Target_of (F . x) ) ) ; :: thesis:

let x be object ; :: thesis:
assume x in dom F ; :: thesis:
then reconsider x0 = x as Element of dom F ;
reconsider G = F . x0 as _Graph ;
take G = G; :: thesis:
thus ( G = F . x & f . x = the_Target_of G ) by A12; :: thesis:

end;

hence f = the_Target_of F by A12, Def7; :: thesis: