let G be non-Dmulti _Graph; :: thesis: for v being Vertex of G holds v .outDegree() = card (v .outNeighbors())
let v be Vertex of G; :: thesis: v .outDegree() = card (v .outNeighbors())
defpred S₁[ object , object ] means $2 DJoins v,$1,G;
A1: for x, y1, y2 being object st x in v .outNeighbors() & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 by Def21;
A2: for x being object st x in v .outNeighbors() holds
ex y being object st S₁[x,y] by Th70;
consider f being Function such that
A3: dom f = v .outNeighbors() and
A4: for x being object st x in v .outNeighbors() 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 .edgesOut() )

proof

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

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

assume y in rng f ; :: thesis: y in v .edgesOut()
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 .edgesOut() by A3, A4, A5, Th59; :: thesis: verum

end;

assume y in v .edgesOut() ; :: thesis: y in rng f
then consider x being set such that
A6: y DJoins v,x,G by Th59;
a7: x in v .outNeighbors() by A6, Th70;
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, A3, FUNCT_1:def 3; :: thesis: verum

end;

then A8: rng f = v .edgesOut() 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_Target_of G) . (f . x1) = x1 & (the_Target_of G) . (f . x1) = x2 ) by Def14;
hence x1 = x2 ; :: thesis: verum

end;

then f is one-to-one by FUNCT_1:def 4;
then card (v .outNeighbors()) = card (v .edgesOut()) by A3, A8, WELLORD2:def 4, CARD_1:5;
hence v .outDegree() = card (v .outNeighbors()) ; :: thesis: verum