let G be non-Dmulti _Graph; :: thesis: for v being Vertex of G holds v .inDegree() = card (v .inNeighbors())
let v be Vertex of G; :: thesis: v .inDegree() = card (v .inNeighbors())
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() )

proof

let y be object ; :: thesis: ( y in rng f iff y in v .edgesIn() )

hereby :: thesis: ( y in v .edgesIn() implies y in rng f )

assume y in rng f ; :: thesis: y in v .edgesIn()
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: verum

end;

assume y in v .edgesIn() ; :: thesis: y in rng f
then consider x being set such that
A6: y DJoins x,v,G by GLIB_000:57;
a7: x in v .inNeighbors() by A6, GLIB_000:69;
then ( x in dom f & S₁[x,f . x] ) by A3, A4;
then y = f . x by A1, A3, A6;
hence y in rng f by a7, FUNCT_1:def 3, A3; :: thesis: verum

end;

then A8: rng f = v .edgesIn() by TARSKI:2;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
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: verum

end;

then f is one-to-one by FUNCT_1:def 4;
then card (v .inNeighbors()) = card (v .edgesIn()) by A3, A8, WELLORD2:def 4, CARD_1:5;
hence v .inDegree() = card (v .inNeighbors()) by GLIB_000:def 42; :: thesis: verum