let G be Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 A10: v = the Target of G . (p . i) ; :: thesis: ex i being 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 A5, A10, FINSEQ_3:25; :: thesis: verum

end;

suppose A11: v = the Source of G . (p . i) ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum

end;

end;