let G be Graph; :: thesis: for v being Element of the carrier 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 Element of NAT st
( 1 <= i & i <= len p & v = the Target of G . (p . i) )
let v be Element of the carrier of G; :: thesis: for p being oriented Chain of G st v <> the Source of G . (p . 1) & v in vertices p holds
ex i being Element of NAT st
( 1 <= i & i <= len p & v = the Target of G . (p . i) )
let p be oriented Chain of G; :: thesis: ( v <> the Source of G . (p . 1) & v in vertices p implies ex i being Element of 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 A1: ( v <> the Source of G . (p . 1) & v in vertices p ) ; :: thesis: ex i being Element of NAT st
( 1 <= i & i <= len p & v = the Target of G . (p . i) )
then consider u being Vertex of G such that
A2: ( v = u & ex i being Element of NAT st
( i in dom p & u in vertices (p /. i) ) ) ;
consider i being Element of NAT such that
A3: ( i in dom p & u in vertices (p /. i) ) by A2;
A4: ( u = the Source of G . (p /. i) or u = the Target of G . (p /. i) ) by A3, TARSKI:def 2;
A5: ( 1 <= i & i <= len p ) by A3, FINSEQ_3:27;

per cases ( v = the Target of G . (p . i) or v = the Source of G . (p . i) ) by A2, A4, A5, FINSEQ_4:24;

suppose A6: v = the Target of G . (p . i) ; :: thesis: ex i being Element of NAT st
( 1 <= i & i <= len p & v = the Target of G . (p . i) )

take i ; :: thesis: ( 1 <= i & i <= len p & v = the Target of G . (p . i) )
thus ( 1 <= i & i <= len p & v = the Target of G . (p . i) ) by A3, A6, FINSEQ_3:27; :: thesis: verum

end;

suppose A7: v = the Source of G . (p . i) ; :: thesis: ex i being Element of NAT st
( 1 <= i & i <= len p & v = the Target of G . (p . i) )

then A8: i > 1 by A1, A5, XXREAL_0:1;
consider j being Nat such that
A9: i = 1 + j by A5, NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A10: j >= 1 by A8, A9, NAT_1:13;
A11: j < len p by A5, A9, NAT_1:13;
take j ; :: thesis: ( 1 <= j & j <= len p & v = the Target of G . (p . j) )
thus ( 1 <= j & j <= len p & v = the Target of G . (p . j) ) by A7, A9, A10, A11, GRAPH_1:def 13; :: thesis: verum

end;

end;