let G be non-Dmulti _Graph; :: thesis:
let v be Vertex of G; :: thesis:
defpred S₁[ object , object ] means $2 DJoins $1,v,G;
A1: for x, y1, y2 being object st x in v .inNeighbors() & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 by GLIB_000:def 21;
A2: for x being object st x in v .inNeighbors() holds
ex y being object st S₁[x,y] by GLIB_000:69;
consider f being Function such that
A3: dom f = v .inNeighbors() and
A4: for x being object st x in v .inNeighbors() holds
S₁[x,f . x] from FUNCT_1:sch 2(A1, A2);
for y being object holds
( y in rng f iff y in v .edgesIn() )

let y be object ; :: thesis:

assume y in rng f ; :: thesis:
then consider x being object such that
A5: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
thus y in v .edgesIn() by A3, A4, A5, GLIB_000:57; :: thesis:

end;

end;

let x1, x2 be object ; :: thesis:
assume ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis:
then ( S₁[x1,f . x1] & S₁[x2,f . x1] ) by A3, A4;
then ( (the_Source_of G) . (f . x1) = x1 & (the_Source_of G) . (f . x1) = x2 ) by GLIB_000:def 14;
hence x1 = x2 ; :: thesis:

end;