let n be non zero Nat; for C1, C2 being n -vertex Cycle-like _Graph holds C2 is C1 -isomorphic
let C1, C2 be n -vertex Cycle-like _Graph; C2 is C1 -isomorphic
per cases
( n = 1 or n <> 1 )
;
suppose
n <> 1
;
C2 is C1 -isomorphic then
(
C1 .order() <> 1 &
C2 .order() <> 1 )
by GLIB_013:def 3;
then A2:
( not
C1 is
_trivial & not
C2 is
_trivial )
by GLIB_000:26;
set e1 = the
Edge of
C1;
set e2 = the
Edge of
C2;
set v1 =
(the_Source_of C1) . the
Edge of
C1;
set w1 =
(the_Target_of C1) . the
Edge of
C1;
set v2 =
(the_Source_of C2) . the
Edge of
C2;
set w2 =
(the_Target_of C2) . the
Edge of
C2;
A3:
( the
Edge of
C1 DJoins (the_Source_of C1) . the
Edge of
C1,
(the_Target_of C1) . the
Edge of
C1,
C1 & the
Edge of
C2 DJoins (the_Source_of C2) . the
Edge of
C2,
(the_Target_of C2) . the
Edge of
C2,
C2 )
by GLIB_000:def 14;
consider P1 being
_finite non
_trivial Path-like _Graph such that A4:
( not the
Edge of
C1 in the_Edges_of P1 &
C1 is
addEdge of
P1,
(the_Source_of C1) . the
Edge of
C1, the
Edge of
C1,
(the_Target_of C1) . the
Edge of
C1 )
and A5:
Endvertices P1 = {((the_Source_of C1) . the Edge of C1),((the_Target_of C1) . the Edge of C1)}
by A2, A3, Th45;
reconsider v1 =
(the_Source_of C1) . the
Edge of
C1,
w1 =
(the_Target_of C1) . the
Edge of
C1 as
Vertex of
P1 by A4, Lm8;
consider P2 being
_finite non
_trivial Path-like _Graph such that A6:
( not the
Edge of
C2 in the_Edges_of P2 &
C2 is
addEdge of
P2,
(the_Source_of C2) . the
Edge of
C2, the
Edge of
C2,
(the_Target_of C2) . the
Edge of
C2 )
and A7:
Endvertices P2 = {((the_Source_of C2) . the Edge of C2),((the_Target_of C2) . the Edge of C2)}
by A2, A3, Th45;
reconsider v2 =
(the_Source_of C2) . the
Edge of
C2,
w2 =
(the_Target_of C2) . the
Edge of
C2 as
Vertex of
P2 by A6, Lm8;
P1 .order() =
C1 .order()
by A4, Lm8
.=
n
by GLIB_013:def 3
;
then A8:
P1 is
n -vertex
by GLIB_013:def 3;
P2 .order() =
C2 .order()
by A6, Lm8
.=
n
by GLIB_013:def 3
;
then
P2 is
n -vertex
by GLIB_013:def 3;
then
P2 is
P1 -isomorphic
by A8, Th32;
then consider F0 being
PGraphMapping of
P1,
P2 such that A9:
F0 is
isomorphism
by GLIB_010:def 23;
A10:
dom (F0 _V) = the_Vertices_of P1
by A9, GLIB_010:def 11;
v1 in Endvertices P1
by A5, TARSKI:def 2;
then 1 =
v1 .degree()
by GLIB_006:56, GLIB_000:174
.=
((F0 _V) /. v1) .degree()
by A9, GLIBPRE0:93
;
then
(F0 _V) /. v1 in {v2,w2}
by A7, GLIB_006:56, GLIB_000:174;
then
(F0 _V) . v1 in {v2,w2}
by A10, PARTFUN1:def 6;
then A11:
(
(F0 _V) . v1 = v2 or
(F0 _V) . v1 = w2 )
by TARSKI:def 2;
w1 in Endvertices P1
by A5, TARSKI:def 2;
then 1 =
w1 .degree()
by GLIB_006:56, GLIB_000:174
.=
((F0 _V) /. w1) .degree()
by A9, GLIBPRE0:93
;
then
(F0 _V) /. w1 in {v2,w2}
by A7, GLIB_006:56, GLIB_000:174;
then
(F0 _V) . w1 in {v2,w2}
by A10, PARTFUN1:def 6;
then A12:
(
(F0 _V) . w1 = v2 or
(F0 _V) . w1 = w2 )
by TARSKI:def 2;
v1 <> w1
then A13:
( (
(F0 _V) . v1 = v2 &
(F0 _V) . w1 = w2 ) or (
(F0 _V) . v1 = w2 &
(F0 _V) . w1 = v2 ) )
by A9, A10, A11, A12, FUNCT_1:def 4;
consider F being
PGraphMapping of
C1,
C2 such that
F = [(F0 _V),((F0 _E) +* ( the Edge of C1 .--> the Edge of C2))]
and
(
F0 is
weak_SG-embedding implies
F is
weak_SG-embedding )
and A14:
(
F0 is
isomorphism implies
F is
isomorphism )
by A4, A6, A10, A13, GLIB_010:153;
thus
C2 is
C1 -isomorphic
by A9, A14, GLIB_010:def 23;
verum end;