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

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

assume A7: f = the_Source_of F ; :: thesis: ( dom f = dom F & ( for x being Element of dom F holds f . x = the_Source_of (F . x) ) )
hence dom f = dom F by Def6; :: thesis: for x being Element of dom F holds f . x = the_Source_of (F . x)
let x be Element of dom F; :: thesis: f . x = the_Source_of (F . x)
consider G being _Graph such that
A8: ( G = F . x & f . x = the_Source_of G ) by A7, Def6;
thus f . x = the_Source_of (F . x) by A8; :: thesis: verum

end;

assume A9: ( dom f = dom F & ( for x being Element of dom F holds f . x = the_Source_of (F . x) ) ) ; :: thesis: f = the_Source_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_Source_of G )

let x be object ; :: thesis: ( x in dom F implies ex G being _Graph st
( G = F . x & f . x = the_Source_of G ) )
assume x in dom F ; :: thesis: ex G being _Graph st
( G = F . x & f . x = the_Source_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_Source_of G )
thus ( G = F . x & f . x = the_Source_of G ) by A9; :: thesis: verum

end;

hence f = the_Source_of F by A9, Def6; :: thesis: verum