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 A1: ( p = pe ^ qe & len pe >= 1 & 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
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;
len p = (len pe) + (len qe) by A1, FINSEQ_1:35;
then A4: len p >= (len pe) + 1 by A1, XREAL_1:9;
then A5: len p > len pe by NAT_1:13;
then A6: len p >= 1 by A1, XXREAL_0:2;
A7: 1 <= len vs by A3, NAT_1:12;
p . (len p) orientedly_joins vs /. (len p),vs /. ((len p) + 1) by A2, A6, 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, A7, FINSEQ_4:24 ;
A9: 1 < (len pe) + 1 by A1, NAT_1:13;
A10: (len pe) + 1 < len vs by A3, A4, NAT_1:13;
A11: p . (len pe) orientedly_joins vs /. (len pe),vs /. ((len pe) + 1) by A1, A2, A5, GRAPH_4:def 5;
the Target of G . (pe . (len pe)) = the Target of G . (p . (len pe)) by A1, Lm1
.= vs /. ((len pe) + 1) by A11, GRAPH_4:def 1
.= vs . ((len pe) + 1) by A9, A10, FINSEQ_4:24 ;
hence the Target of G . (p . (len p)) <> the Target of G . (pe . (len pe)) by A2, A8, A9, A10; :: thesis: the Source of G . (p . 1) <> the Source of G . (qe . 1)
p . 1 orientedly_joins vs /. 1,vs /. (1 + 1) by A2, A6, 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:24 ;
A13: p . ((len pe) + 1) orientedly_joins vs /. ((len pe) + 1),vs /. (((len pe) + 1) + 1) by A2, A4, A9, GRAPH_4:def 5;
A14: the Source of G . (qe . 1) = the Source of G . (p . ((len pe) + 1)) by A1, Lm2
.= vs /. ((len pe) + 1) by A13, GRAPH_4:def 1
.= vs . ((len pe) + 1) by A9, A10, FINSEQ_4:24 ;
assume the Source of G . (p . 1) = the Source of G . (qe . 1) ; :: thesis: contradiction
hence contradiction by A2, A9, A10, A12, A14; :: thesis: verum