let G be Graph; for pe, qe being FinSequence of the carrier' of G
for p being oriented Simple Chain of G st p = pe ^ qe & len pe >= 1 & len qe >= 1 & the Source of G . (p . 1) <> the Target of G . (p . (len p)) holds
( not the Source of G . (p . 1) in vertices qe & not the Target of G . (p . (len p)) in vertices pe )
let pe, qe be FinSequence of the carrier' of G; for p being oriented Simple Chain of G st p = pe ^ qe & len pe >= 1 & len qe >= 1 & the Source of G . (p . 1) <> the Target of G . (p . (len p)) holds
( not the Source of G . (p . 1) in vertices qe & not the Target of G . (p . (len p)) in vertices pe )
let p be oriented Simple Chain of G; ( p = pe ^ qe & len pe >= 1 & len qe >= 1 & the Source of G . (p . 1) <> the Target of G . (p . (len p)) implies ( not the Source of G . (p . 1) in vertices qe & not the Target of G . (p . (len p)) in vertices pe ) )
set FT = the Target of G;
set FS = the Source of G;
assume that
A1:
p = pe ^ qe
and
A2:
len pe >= 1
and
A3:
len qe >= 1
and
A4:
the Source of G . (p . 1) <> the Target of G . (p . (len p))
; ( not the Source of G . (p . 1) in vertices qe & not the Target of G . (p . (len p)) in vertices pe )
consider vs being FinSequence of the carrier of G such that
A5:
vs is_oriented_vertex_seq_of p
and
A6:
for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )
by GRAPH_4:def 7;
A7:
len vs = (len p) + 1
by A5, GRAPH_4:def 5;
then A8:
1 <= len vs
by NAT_1:12;
A9:
len p = (len pe) + (len qe)
by A1, FINSEQ_1:22;
then A10:
len p >= 1
by A2, NAT_1:12;
then
p . 1 orientedly_joins vs /. 1,vs /. (1 + 1)
by A5, GRAPH_4:def 5;
then A11: the Source of G . (p . 1) =
vs /. 1
by GRAPH_4:def 1
.=
vs . 1
by A8, FINSEQ_4:15
;
p . (len p) orientedly_joins vs /. (len p),vs /. ((len p) + 1)
by A5, A10, GRAPH_4:def 5;
then A12: the Target of G . (p . (len p)) =
vs /. ((len p) + 1)
by GRAPH_4:def 1
.=
vs . (len vs)
by A7, A8, FINSEQ_4:15
;
hereby not the Target of G . (p . (len p)) in vertices pe
assume
the
Source of
G . (p . 1) in vertices qe
;
contradictionthen consider x being
Vertex of
G such that A13:
the
Source of
G . (p . 1) = x
and A14:
ex
i being
Nat st
(
i in dom qe &
x in vertices (qe /. i) )
;
consider i being
Nat such that A15:
i in dom qe
and A16:
x in vertices (qe /. i)
by A14;
set k =
(len pe) + i;
A17:
qe /. i =
qe . i
by A15, PARTFUN1:def 6
.=
p . ((len pe) + i)
by A1, A15, FINSEQ_1:def 7
;
1
<= i
by A15, FINSEQ_3:25;
then A18:
1
< i + 1
by NAT_1:13;
i <= len qe
by A15, FINSEQ_3:25;
then A19:
(len pe) + i <= len p
by A9, XREAL_1:7;
then A20:
(len pe) + i <= len vs
by A7, NAT_1:13;
1
+ i <= (len pe) + i
by A2, XREAL_1:7;
then A21:
1
< (len pe) + i
by A18, XXREAL_0:2;
then A22:
p . ((len pe) + i) orientedly_joins vs /. ((len pe) + i),
vs /. (((len pe) + i) + 1)
by A5, A19, GRAPH_4:def 5;
per cases
( x = the Source of G . (p . ((len pe) + i)) or x = the Target of G . (p . ((len pe) + i)) )
by A16, A17, TARSKI:def 2;
suppose A23:
x = the
Source of
G . (p . ((len pe) + i))
;
contradiction the
Source of
G . (p . ((len pe) + i)) =
vs /. ((len pe) + i)
by A22, GRAPH_4:def 1
.=
vs . ((len pe) + i)
by A21, A20, FINSEQ_4:15
;
hence
contradiction
by A4, A6, A11, A12, A13, A21, A20, A23;
verum end; suppose A24:
x = the
Target of
G . (p . ((len pe) + i))
;
contradictionA25:
1
< ((len pe) + i) + 1
by A21, NAT_1:13;
A26:
((len pe) + i) + 1
<= len vs
by A7, A19, XREAL_1:7;
the
Target of
G . (p . ((len pe) + i)) =
vs /. (((len pe) + i) + 1)
by A22, GRAPH_4:def 1
.=
vs . (((len pe) + i) + 1)
by A26, FINSEQ_4:15, NAT_1:12
;
hence
contradiction
by A4, A6, A11, A12, A13, A24, A26, A25;
verum end; end;
end;
hereby verum
assume
the
Target of
G . (p . (len p)) in vertices pe
;
contradictionthen consider x being
Vertex of
G such that A27:
the
Target of
G . (p . (len p)) = x
and A28:
ex
i being
Nat st
(
i in dom pe &
x in vertices (pe /. i) )
;
consider i being
Nat such that A29:
i in dom pe
and A30:
x in vertices (pe /. i)
by A28;
A31:
pe /. i =
pe . i
by A29, PARTFUN1:def 6
.=
p . i
by A1, A29, FINSEQ_1:def 7
;
A32:
i <= len pe
by A29, FINSEQ_3:25;
then A33:
i <= len p
by A9, NAT_1:12;
then A34:
i < len vs
by A7, NAT_1:13;
A35:
1
<= i
by A29, FINSEQ_3:25;
then A36:
p . i orientedly_joins vs /. i,
vs /. (i + 1)
by A5, A33, GRAPH_4:def 5;
per cases
( x = the Source of G . (p . i) or x = the Target of G . (p . i) )
by A30, A31, TARSKI:def 2;
suppose A38:
x = the
Target of
G . (p . i)
;
contradictionA39:
i + 1
<= len vs
by A7, A33, XREAL_1:7;
(
(len pe) + 1
<= (len pe) + (len qe) &
i + 1
<= (len pe) + 1 )
by A3, A32, XREAL_1:7;
then
i + 1
<= len p
by A9, XXREAL_0:2;
then A40:
( 1
<= i + 1 &
i + 1
< len vs )
by A7, NAT_1:12, NAT_1:13;
the
Target of
G . (p . i) =
vs /. (i + 1)
by A36, GRAPH_4:def 1
.=
vs . (i + 1)
by A39, FINSEQ_4:15, NAT_1:12
;
hence
contradiction
by A4, A6, A11, A12, A27, A38, A40;
verum end; end;
end;