let f1, f2 be Function; :: thesis: ( dom f1 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & f1 . x = the_Target_of G ) ) & dom f2 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & f2 . x = the_Target_of G ) ) implies f1 = f2 )
assume that
A28: ( dom f1 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & f1 . x = the_Target_of G ) ) ) and
A29: ( dom f2 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & f2 . x = the_Target_of G ) ) ) ; :: thesis: f1 = f2

now :: thesis: for x being object st x in dom f1 holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume A30: x in dom f1 ; :: thesis: f1 . x = f2 . x
then consider G1 being _Graph such that
A31: ( G1 = F . x & f1 . x = the_Target_of G1 ) by A28;
consider G2 being _Graph such that
A32: ( G2 = F . x & f2 . x = the_Target_of G2 ) by A28, A29, A30;
thus f1 . x = f2 . x by A31, A32; :: thesis: verum

end;

hence f1 = f2 by A28, A29, FUNCT_1:2; :: thesis: verum