let G be _finite _Graph; for v being Denumeration of (the_Vertices_of G) holds
( G .size() = Sum ((G .inDegreeMap()) * v) & G .size() = Sum ((G .outDegreeMap()) * v) )
let v be Denumeration of (the_Vertices_of G); ( G .size() = Sum ((G .inDegreeMap()) * v) & G .size() = Sum ((G .outDegreeMap()) * v) )
deffunc H9( object ) -> set = H7(G,v /. $1);
set f1 = XFS2FS ((G .inDegreeMap()) * v);
set S1 = { H9(i) where i is Nat : i < len (XFS2FS ((G .inDegreeMap()) * v)) } ;
A7:
card (union { H9(i) where i is Nat : i < len (XFS2FS ((G .inDegreeMap()) * v)) } ) = Sum (XFS2FS ((G .inDegreeMap()) * v))
from MSAFREE5:sch 1(A1, A3);
now for y being object holds
( ( y in union { H9(i) where i is Nat : i < len (XFS2FS ((G .inDegreeMap()) * v)) } implies ex x being object st
( x in dom H4(G) & y = H4(G) . x ) ) & ( ex x being object st
( x in dom H4(G) & y = H4(G) . x ) implies y in union { H9(i) where i is Nat : i < len (XFS2FS ((G .inDegreeMap()) * v)) } ) )let y be
object ;
( ( y in union { H9(i) where i is Nat : i < len (XFS2FS ((G .inDegreeMap()) * v)) } implies ex x being object st
( x in dom H4(G) & y = H4(G) . x ) ) & ( ex x being object st
( x in dom H4(G) & y = H4(G) . x ) implies y in union { H9(i) where i is Nat : i < len (XFS2FS ((G .inDegreeMap()) * v)) } ) )hereby ( ex x being object st
( x in dom H4(G) & y = H4(G) . x ) implies y in union { H9(i) where i is Nat : i < len (XFS2FS ((G .inDegreeMap()) * v)) } )
assume
y in union { H9(i) where i is Nat : i < len (XFS2FS ((G .inDegreeMap()) * v)) }
;
ex x being object st
( x in dom H4(G) & y = H4(G) . x )then consider Y being
set such that A8:
(
y in Y &
Y in { H9(i) where i is Nat : i < len (XFS2FS ((G .inDegreeMap()) * v)) } )
by TARSKI:def 4;
consider i being
Nat such that A9:
(
Y = H9(
i) &
i < len (XFS2FS ((G .inDegreeMap()) * v)) )
by A8;
consider x1,
x2,
x3 being
object such that A10:
(
x1 in {(v /. i)} &
x2 in (v /. i) .edgesIn() &
x3 in {1} &
y = [x1,x2,x3] )
by A8, A9, MCART_1:68;
A11:
x1 = v /. i
by A10, TARSKI:def 1;
reconsider x =
[x2,x3] as
object ;
take x =
x;
( x in dom H4(G) & y = H4(G) . x )A12:
x2 in the_Edges_of G
by A10;
then A13:
(
x2 in dom H2(
G) &
x3 in dom (id {1}) )
by A10, Lm4;
x in [:(the_Edges_of G),{1}:]
by A10, ZFMISC_1:def 2;
hence
x in dom H4(
G)
by Lm5;
y = H4(G) . xthus y =
[[x1,x2],x3]
by A10, XTUPLE_0:def 4
.=
[[((the_Target_of G) . x2),x2],x3]
by A10, A11, GLIB_000:56
.=
[[((the_Target_of G) . x2),((id (the_Edges_of G)) . x2)],x3]
by A12, FUNCT_1:18
.=
[(H2(G) . x2),x3]
by A13, FUNCT_3:def 7
.=
[(H2(G) . x2),((id {1}) . x3)]
by A10, FUNCT_1:18
.=
H4(
G)
. (
x2,
x3)
by A13, FUNCT_3:def 8
.=
H4(
G)
. x
by BINOP_1:def 1
;
verum
end; given x being
object such that A14:
(
x in dom H4(
G) &
y = H4(
G)
. x )
;
y in union { H9(i) where i is Nat : i < len (XFS2FS ((G .inDegreeMap()) * v)) }
x in [:(the_Edges_of G),{1}:]
by A14, Lm5;
then consider x2,
x3 being
object such that A15:
(
x2 in the_Edges_of G &
x3 in {1} &
x = [x2,x3] )
by ZFMISC_1:def 2;
A16:
(
x2 in dom H2(
G) &
x3 in dom (id {1}) )
by A15, Lm4;
set x1 =
(the_Target_of G) . x2;
set i =
(v ") . ((the_Target_of G) . x2);
A17:
y =
H4(
G)
. (
x2,
x3)
by A14, A15, BINOP_1:def 1
.=
[(H2(G) . x2),((id {1}) . x3)]
by A16, FUNCT_3:def 8
.=
[(H2(G) . x2),x3]
by A16, FUNCT_1:18
.=
[[((the_Target_of G) . x2),((id (the_Edges_of G)) . x2)],x3]
by A16, FUNCT_3:def 7
.=
[[((the_Target_of G) . x2),x2],x3]
by A15, FUNCT_1:18
.=
[((the_Target_of G) . x2),x2,x3]
by XTUPLE_0:def 4
;
x2 in dom (the_Target_of G)
by A15, FUNCT_2:def 1;
then
(the_Target_of G) . x2 in rng (the_Target_of G)
by FUNCT_1:3;
then reconsider x1 =
(the_Target_of G) . x2 as
Vertex of
G ;
x1 in the_Vertices_of G
;
then
x1 in rng v
by FUNCT_2:def 3;
then A18:
(
v . ((v ") . ((the_Target_of G) . x2)) = x1 &
x1 in dom (v ") )
by FUNCT_1:33, FUNCT_1:35;
then
(v ") . ((the_Target_of G) . x2) in rng (v ")
by FUNCT_1:3;
then A19:
(v ") . ((the_Target_of G) . x2) in dom v
by FUNCT_1:33;
then A20:
(v ") . ((the_Target_of G) . x2) in G .order()
;
then reconsider i =
(v ") . ((the_Target_of G) . x2) as
Ordinal ;
i c= G .order()
by A20, ORDINAL1:def 2;
then reconsider i =
i as
Nat ;
dom (G .inDegreeMap()) = the_Vertices_of G
by PARTFUN1:def 2;
then
x1 in dom (G .inDegreeMap())
;
then
i < len ((G .inDegreeMap()) * v)
by A18, A19, FUNCT_1:11, AFINSQ_1:86;
then
i < len (XFS2FS ((G .inDegreeMap()) * v))
by AFINSQ_1:def 9;
then A21:
(
H9(
i)
in { H9(i) where i is Nat : i < len (XFS2FS ((G .inDegreeMap()) * v)) } &
v /. i = x1 )
by A18, A19, PARTFUN1:def 6;
(
x1 in {x1} &
x2 in x1 .edgesIn() )
by A15, TARSKI:def 1, GLIB_000:56;
then
y in H7(
G,
x1)
by A15, A17, MCART_1:69;
hence
y in union { H9(i) where i is Nat : i < len (XFS2FS ((G .inDegreeMap()) * v)) }
by A21, TARSKI:def 4;
verum end;
then A22:
union { H9(i) where i is Nat : i < len (XFS2FS ((G .inDegreeMap()) * v)) } = rng H4(G)
by FUNCT_1:def 3;
reconsider g = (G .inDegreeMap()) * v as complex-valued XFinSequence ;
thus G .size() =
card [:(the_Edges_of G),{1}:]
by CARD_1:69
.=
card (dom H4(G))
by Lm5
.=
Sum (XFS2FS ((G .inDegreeMap()) * v))
by A7, A22, CARD_1:70
.=
Sum ((G .inDegreeMap()) * v)
by RVSUM_4:64
; G .size() = Sum ((G .outDegreeMap()) * v)
deffunc H10( object ) -> set = H6(G,v /. $1);
set f0 = XFS2FS ((G .outDegreeMap()) * v);
set S0 = { H10(i) where i is Nat : i < len (XFS2FS ((G .outDegreeMap()) * v)) } ;
A29:
card (union { H10(i) where i is Nat : i < len (XFS2FS ((G .outDegreeMap()) * v)) } ) = Sum (XFS2FS ((G .outDegreeMap()) * v))
from MSAFREE5:sch 1(A23, A25);
now for y being object holds
( ( y in union { H10(i) where i is Nat : i < len (XFS2FS ((G .outDegreeMap()) * v)) } implies ex x being object st
( x in dom H3(G) & y = H3(G) . x ) ) & ( ex x being object st
( x in dom H3(G) & y = H3(G) . x ) implies y in union { H10(i) where i is Nat : i < len (XFS2FS ((G .outDegreeMap()) * v)) } ) )let y be
object ;
( ( y in union { H10(i) where i is Nat : i < len (XFS2FS ((G .outDegreeMap()) * v)) } implies ex x being object st
( x in dom H3(G) & y = H3(G) . x ) ) & ( ex x being object st
( x in dom H3(G) & y = H3(G) . x ) implies y in union { H10(i) where i is Nat : i < len (XFS2FS ((G .outDegreeMap()) * v)) } ) )hereby ( ex x being object st
( x in dom H3(G) & y = H3(G) . x ) implies y in union { H10(i) where i is Nat : i < len (XFS2FS ((G .outDegreeMap()) * v)) } )
assume
y in union { H10(i) where i is Nat : i < len (XFS2FS ((G .outDegreeMap()) * v)) }
;
ex x being object st
( x in dom H3(G) & y = H3(G) . x )then consider Y being
set such that A30:
(
y in Y &
Y in { H10(i) where i is Nat : i < len (XFS2FS ((G .outDegreeMap()) * v)) } )
by TARSKI:def 4;
consider i being
Nat such that A31:
(
Y = H10(
i) &
i < len (XFS2FS ((G .outDegreeMap()) * v)) )
by A30;
consider x1,
x2,
x3 being
object such that A32:
(
x1 in {(v /. i)} &
x2 in (v /. i) .edgesOut() &
x3 in {0} &
y = [x1,x2,x3] )
by A30, A31, MCART_1:68;
A33:
x1 = v /. i
by A32, TARSKI:def 1;
reconsider x =
[x2,x3] as
object ;
take x =
x;
( x in dom H3(G) & y = H3(G) . x )A34:
x2 in the_Edges_of G
by A32;
then A35:
(
x2 in dom H1(
G) &
x3 in dom (id {0}) )
by A32, Lm4;
x in [:(the_Edges_of G),{0}:]
by A32, ZFMISC_1:def 2;
hence
x in dom H3(
G)
by Lm5;
y = H3(G) . xthus y =
[[x1,x2],x3]
by A32, XTUPLE_0:def 4
.=
[[((the_Source_of G) . x2),x2],x3]
by A32, A33, GLIB_000:58
.=
[[((the_Source_of G) . x2),((id (the_Edges_of G)) . x2)],x3]
by A34, FUNCT_1:18
.=
[(H1(G) . x2),x3]
by A35, FUNCT_3:def 7
.=
[(H1(G) . x2),((id {0}) . x3)]
by A32, FUNCT_1:18
.=
H3(
G)
. (
x2,
x3)
by A35, FUNCT_3:def 8
.=
H3(
G)
. x
by BINOP_1:def 1
;
verum
end; given x being
object such that A36:
(
x in dom H3(
G) &
y = H3(
G)
. x )
;
y in union { H10(i) where i is Nat : i < len (XFS2FS ((G .outDegreeMap()) * v)) }
x in [:(the_Edges_of G),{0}:]
by A36, Lm5;
then consider x2,
x3 being
object such that A37:
(
x2 in the_Edges_of G &
x3 in {0} &
x = [x2,x3] )
by ZFMISC_1:def 2;
A38:
(
x2 in dom H1(
G) &
x3 in dom (id {0}) )
by A37, Lm4;
set x1 =
(the_Source_of G) . x2;
set i =
(v ") . ((the_Source_of G) . x2);
A39:
y =
H3(
G)
. (
x2,
x3)
by A36, A37, BINOP_1:def 1
.=
[(H1(G) . x2),((id {0}) . x3)]
by A38, FUNCT_3:def 8
.=
[(H1(G) . x2),x3]
by A38, FUNCT_1:18
.=
[[((the_Source_of G) . x2),((id (the_Edges_of G)) . x2)],x3]
by A38, FUNCT_3:def 7
.=
[[((the_Source_of G) . x2),x2],x3]
by A37, FUNCT_1:18
.=
[((the_Source_of G) . x2),x2,x3]
by XTUPLE_0:def 4
;
x2 in dom (the_Source_of G)
by A37, FUNCT_2:def 1;
then
(the_Source_of G) . x2 in rng (the_Source_of G)
by FUNCT_1:3;
then reconsider x1 =
(the_Source_of G) . x2 as
Vertex of
G ;
x1 in the_Vertices_of G
;
then
x1 in rng v
by FUNCT_2:def 3;
then A40:
(
v . ((v ") . ((the_Source_of G) . x2)) = x1 &
x1 in dom (v ") )
by FUNCT_1:33, FUNCT_1:35;
then
(v ") . ((the_Source_of G) . x2) in rng (v ")
by FUNCT_1:3;
then A41:
(v ") . ((the_Source_of G) . x2) in dom v
by FUNCT_1:33;
then A42:
(v ") . ((the_Source_of G) . x2) in G .order()
;
then reconsider i =
(v ") . ((the_Source_of G) . x2) as
Ordinal ;
i c= G .order()
by A42, ORDINAL1:def 2;
then reconsider i =
i as
Nat ;
dom (G .outDegreeMap()) = the_Vertices_of G
by PARTFUN1:def 2;
then
x1 in dom (G .outDegreeMap())
;
then
i < len ((G .outDegreeMap()) * v)
by A40, A41, FUNCT_1:11, AFINSQ_1:86;
then
i < len (XFS2FS ((G .outDegreeMap()) * v))
by AFINSQ_1:def 9;
then A43:
(
H10(
i)
in { H10(i) where i is Nat : i < len (XFS2FS ((G .outDegreeMap()) * v)) } &
v /. i = x1 )
by A40, A41, PARTFUN1:def 6;
(
x1 in {x1} &
x2 in x1 .edgesOut() )
by A37, TARSKI:def 1, GLIB_000:58;
then
y in H6(
G,
x1)
by A37, A39, MCART_1:69;
hence
y in union { H10(i) where i is Nat : i < len (XFS2FS ((G .outDegreeMap()) * v)) }
by A43, TARSKI:def 4;
verum end;
then A44:
union { H10(i) where i is Nat : i < len (XFS2FS ((G .outDegreeMap()) * v)) } = rng H3(G)
by FUNCT_1:def 3;
reconsider g = (G .outDegreeMap()) * v as complex-valued XFinSequence ;
thus G .size() =
card [:(the_Edges_of G),{0}:]
by CARD_1:69
.=
card (dom H3(G))
by Lm5
.=
Sum (XFS2FS ((G .outDegreeMap()) * v))
by A29, A44, CARD_1:70
.=
Sum ((G .outDegreeMap()) * v)
by RVSUM_4:64
; verum