let G1 be non trivial _Graph; :: thesis:
let v be Vertex of G1; :: thesis:
let G2 be removeVertex of G1,v; :: thesis:
assume A1: v is isolated ; :: thesis:
for V being object holds
( V in G1 .componentSet() iff V in (G2 .componentSet()) \/ {{v}} )

proof

let V be object ; :: thesis:

hereby :: thesis:

assume V in G1 .componentSet() ; :: thesis:
then consider v1 being Vertex of G1 such that
A2: V = G1 .reachableFrom v1 by GLIB_002:def 8;

per cases ;

suppose v = v1 ; :: thesis:

then V = {v} by A1, A2, Th55;
then V in {{v}} by TARSKI:def 1;
hence V in (G2 .componentSet()) \/ {{v}} by XBOOLE_0:def 3; :: thesis:

end;

suppose v <> v1 ; :: thesis:

then not v1 in {v} by TARSKI:def 1;
then v1 in (the_Vertices_of G1) \ {v} by XBOOLE_0:def 5;
then reconsider v2 = v1 as Vertex of G2 by GLIB_000:def 37;
for v3 being object st v3 in G1 .reachableFrom v1 holds
v3 in G2 .reachableFrom v2

proof

let v3 be object ; :: thesis:
assume A3: v3 in G1 .reachableFrom v1 ; :: thesis:

per cases ;

suppose A4: v2 <> v3 ; :: thesis:

ex W2 being Walk of G2 st W2 is_Walk_from v2,v3

proof

consider W being Walk of G1 such that
A5: W is_Walk_from v1,v3 by A3, GLIB_002:def 5;
( W .first() = v1 & W .last() = v3 ) by A5, GLIB_001:def 23;
then not W is trivial by A4, GLIB_001:127;
then not v in W .vertices() by A1, GLIB_001:135;
then reconsider W2 = W as Walk of G2 by GLIB_001:171;
take W2 ; :: thesis:
thus W2 is_Walk_from v2,v3 by A5, GLIB_001:19; :: thesis:

end;

hence v3 in G2 .reachableFrom v2 by GLIB_002:def 5; :: thesis:

end;

suppose v2 = v3 ; :: thesis:

hence v3 in G2 .reachableFrom v2 by GLIB_002:9; :: thesis:

end;

end;

end;

then A6: G1 .reachableFrom v1 c= G2 .reachableFrom v2 by TARSKI:def 3;
G2 .reachableFrom v2 c= G1 .reachableFrom v1 by GLIB_002:14;
then G1 .reachableFrom v1 = G2 .reachableFrom v2 by A6, XBOOLE_0:def 10;
then V in G2 .componentSet() by A2, GLIB_002:def 8;
hence V in (G2 .componentSet()) \/ {{v}} by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

assume V in (G2 .componentSet()) \/ {{v}} ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose V in G2 .componentSet() ; :: thesis:

then consider v2 being Vertex of G2 such that
A7: V = G2 .reachableFrom v2 by GLIB_002:def 8;
reconsider v1 = v2 as Vertex of G1 by GLIB_000:42;
for v3 being object st v3 in G1 .reachableFrom v1 holds
v3 in G2 .reachableFrom v2

proof

let v3 be object ; :: thesis:
assume A8: v3 in G1 .reachableFrom v1 ; :: thesis:

per cases ;

suppose A9: v2 <> v3 ; :: thesis:

ex W2 being Walk of G2 st W2 is_Walk_from v2,v3

proof

consider W being Walk of G1 such that
A10: W is_Walk_from v1,v3 by A8, GLIB_002:def 5;
( W .first() = v1 & W .last() = v3 ) by A10, GLIB_001:def 23;
then not W is trivial by A9, GLIB_001:127;
then not v in W .vertices() by A1, GLIB_001:135;
then reconsider W2 = W as Walk of G2 by GLIB_001:171;
take W2 ; :: thesis:
thus W2 is_Walk_from v2,v3 by A10, GLIB_001:19; :: thesis:

end;

hence v3 in G2 .reachableFrom v2 by GLIB_002:def 5; :: thesis:

end;

suppose v2 = v3 ; :: thesis:

hence v3 in G2 .reachableFrom v2 by GLIB_002:9; :: thesis:

end;

end;

end;

then A11: G1 .reachableFrom v1 c= G2 .reachableFrom v2 by TARSKI:def 3;
G2 .reachableFrom v2 c= G1 .reachableFrom v1 by GLIB_002:14;
then G1 .reachableFrom v1 = G2 .reachableFrom v2 by A11, XBOOLE_0:def 10;
hence V in G1 .componentSet() by A7, GLIB_002:def 8; :: thesis:

end;

suppose V in {{v}} ; :: thesis:

then V = {v} by TARSKI:def 1;
then V = G1 .reachableFrom v by A1, Th55;
hence V in G1 .componentSet() by GLIB_002:def 8; :: thesis:

end;

end;

end;

hence A12: G1 .componentSet() = (G2 .componentSet()) \/ {{v}} by TARSKI:2; :: thesis:
not {v} in G2 .componentSet()

proof

assume {v} in G2 .componentSet() ; :: thesis:
then consider v2 being Vertex of G2 such that
A13: {v} = G2 .reachableFrom v2 by GLIB_002:def 8;
v in G2 .reachableFrom v2 by A13, TARSKI:def 1;
then A14: v in the_Vertices_of G2 ;
v in {v} by TARSKI:def 1;
then not v in (the_Vertices_of G1) \ {v} by XBOOLE_0:def 5;
hence contradiction by A14, GLIB_000:47; :: thesis:

end;

then A15: G2 .componentSet() misses {{v}} by ZFMISC_1:50;
thus G1 .numComponents() = card (G1 .componentSet()) by GLIB_002:def 9
.= (card (G2 .componentSet())) +` (card {{v}}) by A12, A15, CARD_2:35
.= (G2 .numComponents()) +` (card {{v}}) by GLIB_002:def 9
.= (G2 .numComponents()) +` 1 by CARD_2:42 ; :: thesis: