let G be Graph; for c being Chain of G
for p being FinSequence of the carrier of G st c is cyclic & p is_vertex_seq_of c holds
p . 1 = p . (len p)
let c be Chain of G; for p being FinSequence of the carrier of G st c is cyclic & p is_vertex_seq_of c holds
p . 1 = p . (len p)
let p be FinSequence of the carrier of G; ( c is cyclic & p is_vertex_seq_of c implies p . 1 = p . (len p) )
assume that
A1:
c is cyclic
and
A2:
p is_vertex_seq_of c
; p . 1 = p . (len p)
consider P being FinSequence of the carrier of G such that
A3:
P is_vertex_seq_of c
and
A4:
P . 1 = P . (len P)
by A1;
per cases
( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) or ( not card the carrier of G = 1 & not ( c <> {} & not c alternates_vertices_in G ) ) )
;
suppose A5:
( not
card the
carrier of
G = 1 & not (
c <> {} & not
c alternates_vertices_in G ) )
;
p . 1 = p . (len p)A6:
len p = (len c) + 1
by A2;
A7:
len P = (len c) + 1
by A3;
now p . 1 = p . (len p)per cases
( ( card the carrier of G <> 1 & c = {} ) or ( card the carrier of G <> 1 & c alternates_vertices_in G ) )
by A5;
suppose A8:
(
card the
carrier of
G <> 1 &
c alternates_vertices_in G )
;
p . 1 = p . (len p)then A9:
(
p is
TwoValued &
p is
Alternating &
P is
TwoValued &
P is
Alternating )
by A2, A3, GRAPH_2:37;
now ( p <> P implies p . 1 = p . (len p) )set S = the
Source of
G;
set T = the
Target of
G;
assume
p <> P
;
p . 1 = p . (len p)A10:
rng p = {( the Source of G . (c . 1)),( the Target of G . (c . 1))}
by A2, A8, GRAPH_2:36;
A11:
1
<= len p
by A6, NAT_1:11;
then
len p in dom p
by FINSEQ_3:25;
then
p . (len p) in rng p
by FUNCT_1:def 3;
then A12:
(
p . (len p) = the
Source of
G . (c . 1) or
p . (len p) = the
Target of
G . (c . 1) )
by A10, TARSKI:def 2;
A13:
rng P = {( the Source of G . (c . 1)),( the Target of G . (c . 1))}
by A3, A8, GRAPH_2:36;
1
in dom P
by A6, A7, A11, FINSEQ_3:25;
then
P . 1
in rng p
by A10, A13, FUNCT_1:def 3;
then A14:
(
P . 1
= the
Source of
G . (c . 1) or
P . 1
= the
Target of
G . (c . 1) )
by A10, TARSKI:def 2;
1
in dom p
by A11, FINSEQ_3:25;
then
p . 1
in rng p
by FUNCT_1:def 3;
then
(
p . 1
= the
Source of
G . (c . 1) or
p . 1
= the
Target of
G . (c . 1) )
by A10, TARSKI:def 2;
hence
p . 1
= p . (len p)
by A4, A6, A7, A9, A10, A13, A11, A12, A14, FINSEQ_6:147;
verum end; hence
p . 1
= p . (len p)
by A4;
verum end; end; end; hence
p . 1
= p . (len p)
;
verum end; end;