let T be non _trivial Tree-like _Graph; for v being Vertex of T
for F being removeVertex of T,v holds F .numComponents() = v .degree()
let v be Vertex of T; for F being removeVertex of T,v holds F .numComponents() = v .degree()
let F be removeVertex of T,v; F .numComponents() = v .degree()
deffunc H1( Vertex of F) -> Element of K32((the_Vertices_of F)) = F .reachableFrom $1;
A1:
for w being Vertex of F holds H1(w) in F .componentSet()
by GLIB_002:def 8;
consider h9 being Function of (the_Vertices_of F),(F .componentSet()) such that
A2:
for w being Vertex of F holds h9 . w = H1(w)
from FUNCT_2:sch 8(A1);
set h = h9 | (v .allNeighbors());
then A5:
dom (h9 | (v .allNeighbors())) = v .allNeighbors()
by TARSKI:def 3, RELAT_1:62;
now for y being object st y in F .componentSet() holds
y in rng (h9 | (v .allNeighbors()))let y be
object ;
( y in F .componentSet() implies y in rng (h9 | (v .allNeighbors())) )assume
y in F .componentSet()
;
y in rng (h9 | (v .allNeighbors()))then consider w being
Vertex of
F such that A7:
y = F .reachableFrom w
by GLIB_002:def 8;
the_Vertices_of F c= the_Vertices_of T
;
then reconsider u =
w as
Vertex of
T by TARSKI:def 3;
consider W being
Walk of
T such that A8:
W is_Walk_from u,
v
by GLIB_002:def 1;
set P = the
Path of
W;
A9:
the
Path of
W is_Walk_from u,
v
by A8, GLIB_001:160;
(
the_Vertices_of F = (the_Vertices_of T) \ {v} &
v in the_Vertices_of T )
by GLIB_000:47;
then
u <> v
by ZFMISC_1:56;
then A10:
the
Path of
W .first() <> v
by A9, GLIB_001:def 23;
then
the
Path of
W .first() <> the
Path of
W .last()
by A9, GLIB_001:def 23;
then A11:
3
<= len the
Path of
W
by GLIB_001:125, GLIB_001:127;
then reconsider m =
(len the Path of W) - 2 as
Element of
NAT by XXREAL_0:2, INT_1:5;
A12:
m < (len the Path of W) - 0
by XREAL_1:15;
A13:
(
m is
odd & 1 is
odd )
by POLYFORM:4, POLYFORM:5;
then
the
Path of
W . (m + 1) Joins the
Path of
W . m, the
Path of
W . (m + 2),
T
by A12, GLIB_001:def 3;
then
the
Path of
W . (m + 1) Joins the
Path of
W .last() , the
Path of
W . m,
T
by GLIB_000:14;
then
the
Path of
W . (m + 1) Joins v, the
Path of
W . m,
T
by A9, GLIB_001:def 23;
then A14:
the
Path of
W . m in dom (h9 | (v .allNeighbors()))
by A5, GLIB_000:71;
set P9 = the
Path of
W .cut (1,
m);
A15:
3
- 2
<= m
by A11, XREAL_1:9;
A16:
m <= (len the Path of W) - 0
by XREAL_1:10;
A17:
the
Path of
W .cut (1,
m)
is_Walk_from the
Path of
W . 1, the
Path of
W . m
by A13, A15, A16, GLIB_001:37;
not
v in ( the Path of W .cut (1,m)) .vertices()
proof
assume
v in ( the Path of W .cut (1,m)) .vertices()
;
contradiction
then consider n being
odd Element of
NAT such that A18:
(
n <= len ( the Path of W .cut (1,m)) &
( the Path of W .cut (1,m)) . n = v )
by GLIB_001:87;
reconsider n1 =
n - 1 as
Nat by CHORD:1;
reconsider n1 =
n1 as
Element of
NAT by ORDINAL1:def 12;
A19:
n1 + 1
< (len ( the Path of W .cut (1,m))) + 1
by A18, NAT_1:13;
then
n1 < len ( the Path of W .cut (1,m))
by XREAL_1:6;
then A20:
( the Path of W .cut (1,m)) . (n1 + 1) = the
Path of
W . (1 + n1)
by A13, A15, A16, GLIB_001:36;
A21:
(len ( the Path of W .cut (1,m))) + 1
= m + 1
by A13, A15, A16, GLIB_001:36;
m + 1
<= len the
Path of
W
by A12, NAT_1:13;
then A22:
n < len the
Path of
W
by A19, A21, XXREAL_0:2;
the
Path of
W . (len the Path of W) =
the
Path of
W .last()
.=
the
Path of
W . n
by A9, A18, A20, GLIB_001:def 23
;
hence
contradiction
by A10, A18, A20, A22, GLIB_001:def 28;
verum
end; then reconsider P9 = the
Path of
W .cut (1,
m) as
Walk of
F by GLIB_001:171;
P9 is_Walk_from the
Path of
W .first() , the
Path of
W . m
by A17, GLIB_001:19;
then A23:
P9 is_Walk_from u, the
Path of
W . m
by A9, GLIB_001:def 23;
then reconsider z = the
Path of
W . m as
Vertex of
F by GLIB_001:18;
z in F .reachableFrom w
by A23, GLIB_002:def 5;
then
y = F .reachableFrom z
by A7, GLIB_002:12;
then
h9 . ( the Path of W . m) = y
by A2;
then
(h9 | (v .allNeighbors())) . ( the Path of W . m) = y
by A14, FUNCT_1:47;
hence
y in rng (h9 | (v .allNeighbors()))
by A14, FUNCT_1:def 3;
verum end;
then
F .componentSet() c= rng (h9 | (v .allNeighbors()))
by TARSKI:def 3;
then A24:
F .componentSet() = rng (h9 | (v .allNeighbors()))
by XBOOLE_0:def 10;
now for x1, x2 being object st x1 in dom (h9 | (v .allNeighbors())) & x2 in dom (h9 | (v .allNeighbors())) & (h9 | (v .allNeighbors())) . x1 = (h9 | (v .allNeighbors())) . x2 holds
not x1 <> x2let x1,
x2 be
object ;
( x1 in dom (h9 | (v .allNeighbors())) & x2 in dom (h9 | (v .allNeighbors())) & (h9 | (v .allNeighbors())) . x1 = (h9 | (v .allNeighbors())) . x2 implies not x1 <> x2 )assume A25:
(
x1 in dom (h9 | (v .allNeighbors())) &
x2 in dom (h9 | (v .allNeighbors())) &
(h9 | (v .allNeighbors())) . x1 = (h9 | (v .allNeighbors())) . x2 &
x1 <> x2 )
;
contradictionthen reconsider x1 =
x1,
x2 =
x2 as
Vertex of
F ;
A26:
(
(h9 | (v .allNeighbors())) . x1 = h9 . x1 &
(h9 | (v .allNeighbors())) . x2 = h9 . x2 )
by A25, FUNCT_1:47;
(
h9 . x1 = H1(
x1) &
h9 . x2 = H1(
x2) )
by A2;
then A27:
x2 in H1(
x1)
by A25, A26, GLIB_002:9;
set C = the
inducedSubgraph of
F,
H1(
x1);
the_Vertices_of the
inducedSubgraph of
F,
H1(
x1)
= H1(
x1)
by GLIB_000:def 37;
then
(
x2 in the_Vertices_of the
inducedSubgraph of
F,
H1(
x1) &
x1 in the_Vertices_of the
inducedSubgraph of
F,
H1(
x1) )
by A27, GLIB_002:9;
hence
contradiction
by A5, A25, Lm1;
verum end;
then A29:
h9 | (v .allNeighbors()) is one-to-one
by FUNCT_1:def 4;
thus F .numComponents() =
card (F .componentSet())
by GLIB_002:def 9
.=
card (dom (h9 | (v .allNeighbors())))
by A24, A29, CARD_1:70
.=
v .degree()
by A5, GLIB_000:111
; verum