let G1, G2 be _Graph; for F being non empty one-to-one PGraphMapping of G1,G2
for H2 being connected Subgraph of rng F
for H1 being inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) holds H1 is connected
let F be non empty one-to-one PGraphMapping of G1,G2; for H2 being connected Subgraph of rng F
for H1 being inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) holds H1 is connected
let H2 be connected Subgraph of rng F; for H1 being inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) holds H1 is connected
let H1 be inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2); H1 is connected
now for v1, w1 being Vertex of H1 ex W1 being Walk of H1 st W1 is_Walk_from v1,w1let v1,
w1 be
Vertex of
H1;
ex W1 being Walk of H1 st W1 is_Walk_from v1,w1
H2 is
Subgraph of
G2
by GLIB_000:43;
then A1:
(F _E) " (the_Edges_of H2) c= G1 .edgesBetween ((F _V) " (the_Vertices_of H2))
by Th99;
set v = the
Vertex of
H2;
the
Vertex of
H2 in the_Vertices_of H2
;
then
the
Vertex of
H2 in the_Vertices_of (rng F)
;
then
the
Vertex of
H2 in rng (F _V)
by GLIB_010:54;
then consider x being
object such that A2:
(
x in dom (F _V) &
(F _V) . x = the
Vertex of
H2 )
by FUNCT_1:def 3;
x in (F _V) " (the_Vertices_of H2)
by A2, FUNCT_1:def 7;
then
(
the_Vertices_of H1 = (F _V) " (the_Vertices_of H2) &
the_Edges_of H1 = (F _E) " (the_Edges_of H2) )
by A1, GLIB_000:def 37;
then A3:
(
v1 in dom (F _V) &
(F _V) . v1 in the_Vertices_of H2 &
w1 in dom (F _V) &
(F _V) . w1 in the_Vertices_of H2 )
by FUNCT_1:def 7;
then consider W2 being
Walk of
H2 such that A4:
W2 is_Walk_from (F _V) . v1,
(F _V) . w1
by GLIB_002:def 1;
reconsider W3 =
W2 as
F -valued Walk of
G2 by Th108;
reconsider W1 =
F " W3 as
Walk of
H1 by Th109;
take W1 =
W1;
W1 is_Walk_from v1,w1
W3 is_Walk_from (F _V) . v1,
(F _V) . w1
by A4, GLIB_001:19;
then
F " W3 is_Walk_from ((F ") _V) . ((F _V) . v1),
((F ") _V) . ((F _V) . w1)
by Th97;
then
W1 is_Walk_from ((F ") _V) . ((F _V) . v1),
((F ") _V) . ((F _V) . w1)
by GLIB_001:19;
then
W1 is_Walk_from v1,
((F _V) ") . ((F _V) . w1)
by A3, FUNCT_1:34;
hence
W1 is_Walk_from v1,
w1
by A3, FUNCT_1:34;
verum end;
hence
H1 is connected
by GLIB_002:def 1; verum