let G be Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 A1: ( p = pe ^ qe & len pe >= 1 & len qe >= 1 & the Source of G . (p . 1) <> the Target of G . (p . (len p)) ) ; :: thesis: ( 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
A2: ( vs is_oriented_vertex_seq_of p & ( for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) ) ) by GRAPH_4:def 7;
A3: ( len vs = (len p) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds
p . n orientedly_joins vs /. n,vs /. (n + 1) ) ) by A2, GRAPH_4:def 5;
A4: len p = (len pe) + (len qe) by A1, FINSEQ_1:35;
then A5: len p >= 1 by A1, NAT_1:12;
A6: 1 <= len vs by A3, NAT_1:12;
p . 1 orientedly_joins vs /. 1,vs /. (1 + 1) by A2, A5, GRAPH_4:def 5;
then A7: the Source of G . (p . 1) = vs /. 1 by GRAPH_4:def 1
.= vs . 1 by A6, FINSEQ_4:24 ;
p . (len p) orientedly_joins vs /. (len p),vs /. ((len p) + 1) by A2, A5, GRAPH_4:def 5;
then A8: the Target of G . (p . (len p)) = vs /. ((len p) + 1) by GRAPH_4:def 1
.= vs . (len vs) by A3, A6, FINSEQ_4:24 ;

hereby :: thesis: not the Target of G . (p . (len p)) in vertices pe

assume the Source of G . (p . 1) in vertices qe ; :: thesis: contradiction
then consider x being Vertex of G such that
A9: ( the Source of G . (p . 1) = x & ex i being Element of NAT st
( i in dom qe & x in vertices (qe /. i) ) ) ;
consider i being Element of NAT such that
A10: ( i in dom qe & x in vertices (qe /. i) ) by A9;
set k = (len pe) + i;
A11: ( 1 <= i & i <= len qe ) by A10, FINSEQ_3:27;
A12: qe /. i = qe . i by A10, PARTFUN1:def 8
.= p . ((len pe) + i) by A1, A10, FINSEQ_1:def 7 ;
A13: (len pe) + i <= len p by A4, A11, XREAL_1:9;
A14: 1 + i <= (len pe) + i by A1, XREAL_1:9;
1 < i + 1 by A11, NAT_1:13;
then A15: 1 < (len pe) + i by A14, XXREAL_0:2;
A16: (len pe) + i <= len vs by A3, A13, NAT_1:13;
A17: p . ((len pe) + i) orientedly_joins vs /. ((len pe) + i),vs /. (((len pe) + i) + 1) by A2, A13, A15, 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 A10, A12, TARSKI:def 2;

suppose A18: x = the Source of G . (p . ((len pe) + i)) ; :: thesis: contradiction

the Source of G . (p . ((len pe) + i)) = vs /. ((len pe) + i) by A17, GRAPH_4:def 1
.= vs . ((len pe) + i) by A15, A16, FINSEQ_4:24 ;
hence contradiction by A1, A2, A7, A8, A9, A15, A16, A18; :: thesis: verum

end;

suppose A19: x = the Target of G . (p . ((len pe) + i)) ; :: thesis: contradiction

A20: ((len pe) + i) + 1 <= len vs by A3, A13, XREAL_1:9;
A21: 1 < ((len pe) + i) + 1 by A15, NAT_1:13;
the Target of G . (p . ((len pe) + i)) = vs /. (((len pe) + i) + 1) by A17, GRAPH_4:def 1
.= vs . (((len pe) + i) + 1) by A20, FINSEQ_4:24, NAT_1:12 ;
hence contradiction by A1, A2, A7, A8, A9, A19, A20, A21; :: thesis: verum

end;

end;

end;

hereby :: thesis: verum

assume the Target of G . (p . (len p)) in vertices pe ; :: thesis: contradiction
then consider x being Vertex of G such that
A22: ( the Target of G . (p . (len p)) = x & ex i being Element of NAT st
( i in dom pe & x in vertices (pe /. i) ) ) ;
consider i being Element of NAT such that
A23: ( i in dom pe & x in vertices (pe /. i) ) by A22;
A24: ( 1 <= i & i <= len pe ) by A23, FINSEQ_3:27;
A25: pe /. i = pe . i by A23, PARTFUN1:def 8
.= p . i by A1, A23, FINSEQ_1:def 7 ;
A26: i <= len p by A4, A24, NAT_1:12;
then A27: p . i orientedly_joins vs /. i,vs /. (i + 1) by A2, A24, GRAPH_4:def 5;
A28: i < len vs by A3, A26, NAT_1:13;

per cases ( x = the Source of G . (p . i) or x = the Target of G . (p . i) ) by A23, A25, TARSKI:def 2;

suppose A29: x = the Source of G . (p . i) ; :: thesis: contradiction

the Source of G . (p . i) = vs /. i by A27, GRAPH_4:def 1
.= vs . i by A24, A28, FINSEQ_4:24 ;
hence contradiction by A1, A2, A8, A22, A24, A28, A29; :: thesis: verum

end;

suppose A30: x = the Target of G . (p . i) ; :: thesis: contradiction

A31: 1 <= i + 1 by NAT_1:12;
A32: i + 1 <= len vs by A3, A26, XREAL_1:9;
A33: (len pe) + 1 <= (len pe) + (len qe) by A1, XREAL_1:9;
i + 1 <= (len pe) + 1 by A24, XREAL_1:9;
then i + 1 <= len p by A4, A33, XXREAL_0:2;
then A34: i + 1 < len vs by A3, NAT_1:13;
the Target of G . (p . i) = vs /. (i + 1) by A27, GRAPH_4:def 1
.= vs . (i + 1) by A32, FINSEQ_4:24, NAT_1:12 ;
hence contradiction by A1, A2, A7, A8, A22, A30, A31, A34; :: thesis: verum

end;

end;

end;