let f be Function; :: thesis: ( f = the_Target_of F iff ( dom f = dom F & ( for x being Element of dom F holds f . x = the_Target_of (F . x) ) ) )

hereby :: thesis: ( dom f = dom F & ( for x being Element of dom F holds f . x = the_Target_of (F . x) ) implies f = the_Target_of F )

assume A10: f = the_Target_of F ; :: thesis: ( dom f = dom F & ( for x being Element of dom F holds f . x = the_Target_of (F . x) ) )
hence dom f = dom F by Def7; :: thesis: for x being Element of dom F holds f . x = the_Target_of (F . x)
let x be Element of dom F; :: thesis: f . x = the_Target_of (F . x)
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: verum

end;

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

now :: thesis: for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & f . x = the_Target_of G )

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

end;

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