let G be Graph; for v being Element of G
for p being oriented Chain of G st v <> the Source of G . (p . 1) & v in vertices p holds
ex i being Nat st
( 1 <= i & i <= len p & v = the Target of G . (p . i) )
let v be Element of G; for p being oriented Chain of G st v <> the Source of G . (p . 1) & v in vertices p holds
ex i being Nat st
( 1 <= i & i <= len p & v = the Target of G . (p . i) )
let p be oriented Chain of G; ( v <> the Source of G . (p . 1) & v in vertices p implies ex i being Nat st
( 1 <= i & i <= len p & v = the Target of G . (p . i) ) )
set FT = the Target of G;
set FS = the Source of G;
assume that
A1:
v <> the Source of G . (p . 1)
and
A2:
v in vertices p
; ex i being Nat st
( 1 <= i & i <= len p & v = the Target of G . (p . i) )
consider u being Vertex of G such that
A3:
v = u
and
A4:
ex i being Nat st
( i in dom p & u in vertices (p /. i) )
by A2;
consider i being Nat such that
A5:
i in dom p
and
A6:
u in vertices (p /. i)
by A4;
A7:
( u = the Source of G . (p /. i) or u = the Target of G . (p /. i) )
by A6, TARSKI:def 2;
A8:
1 <= i
by A5, FINSEQ_3:25;
A9:
i <= len p
by A5, FINSEQ_3:25;
per cases
( v = the Target of G . (p . i) or v = the Source of G . (p . i) )
by A3, A7, A8, A9, FINSEQ_4:15;
suppose A11:
v = the
Source of
G . (p . i)
;
ex i being Nat st
( 1 <= i & i <= len p & v = the Target of G . (p . i) )consider j being
Nat such that A12:
i = 1
+ j
by A8, NAT_1:10;
reconsider j =
j as
Element of
NAT by ORDINAL1:def 12;
A13:
j < len p
by A9, A12, NAT_1:13;
take
j
;
( 1 <= j & j <= len p & v = the Target of G . (p . j) )
i > 1
by A1, A8, A11, XXREAL_0:1;
then
j >= 1
by A12, NAT_1:13;
hence
( 1
<= j &
j <= len p &
v = the
Target of
G . (p . j) )
by A11, A12, A13, GRAPH_1:def 15;
verum end;