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