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 holds

( the Target of G . (p . (len p)) <> the Target of G . (pe . (len pe)) & the Source of G . (p . 1) <> the Source of G . (qe . 1) )

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 holds

( the Target of G . (p . (len p)) <> the Target of G . (pe . (len pe)) & the Source of G . (p . 1) <> the Source of G . (qe . 1) )

let p be oriented Simple Chain of G; :: thesis: ( p = pe ^ qe & len pe >= 1 & len qe >= 1 implies ( the Target of G . (p . (len p)) <> the Target of G . (pe . (len pe)) & the Source of G . (p . 1) <> the Source of G . (qe . 1) ) )

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 ; :: thesis: ( the Target of G . (p . (len p)) <> the Target of G . (pe . (len pe)) & the Source of G . (p . 1) <> the Source of G . (qe . 1) )

consider vs being FinSequence of the carrier of G such that

A4: vs is_oriented_vertex_seq_of p and

A5: 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;

A6: len vs = (len p) + 1 by A4, GRAPH_4:def 5;

then A7: 1 <= len vs by NAT_1:12;

len p = (len pe) + (len qe) by A1, FINSEQ_1:22;

then A8: len p >= (len pe) + 1 by A3, XREAL_1:7;

then A9: (len pe) + 1 < len vs by A6, NAT_1:13;

A10: len p > len pe by A8, NAT_1:13;

then A11: len p >= 1 by A2, XXREAL_0:2;

then p . 1 orientedly_joins vs /. 1,vs /. (1 + 1) by A4, GRAPH_4:def 5;

then A12: the Source of G . (p . 1) = vs /. 1 by GRAPH_4:def 1

.= vs . 1 by A7, FINSEQ_4:15 ;

A13: p . (len pe) orientedly_joins vs /. (len pe),vs /. ((len pe) + 1) by A2, A4, A10, GRAPH_4:def 5;

p . (len p) orientedly_joins vs /. (len p),vs /. ((len p) + 1) by A4, A11, GRAPH_4:def 5;

then A14: the Target of G . (p . (len p)) = vs /. ((len p) + 1) by GRAPH_4:def 1

.= vs . (len vs) by A6, A7, FINSEQ_4:15 ;

A15: 1 < (len pe) + 1 by A2, NAT_1:13;

then A16: p . ((len pe) + 1) orientedly_joins vs /. ((len pe) + 1),vs /. (((len pe) + 1) + 1) by A4, A8, GRAPH_4:def 5;

the Target of G . (pe . (len pe)) = the Target of G . (p . (len pe)) by A1, A2, Lm1

.= vs /. ((len pe) + 1) by A13, GRAPH_4:def 1

.= vs . ((len pe) + 1) by A15, A9, FINSEQ_4:15 ;

hence the Target of G . (p . (len p)) <> the Target of G . (pe . (len pe)) by A5, A14, A15, A9; :: thesis: the Source of G . (p . 1) <> the Source of G . (qe . 1)

assume A17: the Source of G . (p . 1) = the Source of G . (qe . 1) ; :: thesis: contradiction

the Source of G . (qe . 1) = the Source of G . (p . ((len pe) + 1)) by A1, A3, Lm2

.= vs /. ((len pe) + 1) by A16, GRAPH_4:def 1

.= vs . ((len pe) + 1) by A15, A9, FINSEQ_4:15 ;

hence contradiction by A5, A15, A9, A12, A17; :: thesis: verum

for p being oriented Simple Chain of G st p = pe ^ qe & len pe >= 1 & len qe >= 1 holds

( the Target of G . (p . (len p)) <> the Target of G . (pe . (len pe)) & the Source of G . (p . 1) <> the Source of G . (qe . 1) )

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 holds

( the Target of G . (p . (len p)) <> the Target of G . (pe . (len pe)) & the Source of G . (p . 1) <> the Source of G . (qe . 1) )

let p be oriented Simple Chain of G; :: thesis: ( p = pe ^ qe & len pe >= 1 & len qe >= 1 implies ( the Target of G . (p . (len p)) <> the Target of G . (pe . (len pe)) & the Source of G . (p . 1) <> the Source of G . (qe . 1) ) )

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 ; :: thesis: ( the Target of G . (p . (len p)) <> the Target of G . (pe . (len pe)) & the Source of G . (p . 1) <> the Source of G . (qe . 1) )

consider vs being FinSequence of the carrier of G such that

A4: vs is_oriented_vertex_seq_of p and

A5: 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;

A6: len vs = (len p) + 1 by A4, GRAPH_4:def 5;

then A7: 1 <= len vs by NAT_1:12;

len p = (len pe) + (len qe) by A1, FINSEQ_1:22;

then A8: len p >= (len pe) + 1 by A3, XREAL_1:7;

then A9: (len pe) + 1 < len vs by A6, NAT_1:13;

A10: len p > len pe by A8, NAT_1:13;

then A11: len p >= 1 by A2, XXREAL_0:2;

then p . 1 orientedly_joins vs /. 1,vs /. (1 + 1) by A4, GRAPH_4:def 5;

then A12: the Source of G . (p . 1) = vs /. 1 by GRAPH_4:def 1

.= vs . 1 by A7, FINSEQ_4:15 ;

A13: p . (len pe) orientedly_joins vs /. (len pe),vs /. ((len pe) + 1) by A2, A4, A10, GRAPH_4:def 5;

p . (len p) orientedly_joins vs /. (len p),vs /. ((len p) + 1) by A4, A11, GRAPH_4:def 5;

then A14: the Target of G . (p . (len p)) = vs /. ((len p) + 1) by GRAPH_4:def 1

.= vs . (len vs) by A6, A7, FINSEQ_4:15 ;

A15: 1 < (len pe) + 1 by A2, NAT_1:13;

then A16: p . ((len pe) + 1) orientedly_joins vs /. ((len pe) + 1),vs /. (((len pe) + 1) + 1) by A4, A8, GRAPH_4:def 5;

the Target of G . (pe . (len pe)) = the Target of G . (p . (len pe)) by A1, A2, Lm1

.= vs /. ((len pe) + 1) by A13, GRAPH_4:def 1

.= vs . ((len pe) + 1) by A15, A9, FINSEQ_4:15 ;

hence the Target of G . (p . (len p)) <> the Target of G . (pe . (len pe)) by A5, A14, A15, A9; :: thesis: the Source of G . (p . 1) <> the Source of G . (qe . 1)

assume A17: the Source of G . (p . 1) = the Source of G . (qe . 1) ; :: thesis: contradiction

the Source of G . (qe . 1) = the Source of G . (p . ((len pe) + 1)) by A1, A3, Lm2

.= vs /. ((len pe) + 1) by A16, GRAPH_4:def 1

.= vs . ((len pe) + 1) by A15, A9, FINSEQ_4:15 ;

hence contradiction by A5, A15, A9, A12, A17; :: thesis: verum