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 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)) ; :: 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
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 :: 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
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)) ; :: thesis: 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; :: thesis: verum

end;

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

A25: 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; :: 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
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 A37: x = the Source of G . (p . i) ; :: thesis: contradiction

the Source of G . (p . i) = vs /. i by A36, GRAPH_4:def 1
.= vs . i by A35, A34, FINSEQ_4:15 ;
hence contradiction by A4, A6, A12, A27, A35, A34, A37; :: thesis: verum

end;

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

A39: 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; :: thesis: verum

end;

end;

end;