let G be Graph; :: thesis: for p1, p2 being Path of G
for vs1, vs2 being FinSequence of the carrier of G st rng p1 misses rng p2 & vs1 is_vertex_seq_of p1 & vs2 is_vertex_seq_of p2 & vs1 . (len vs1) = vs2 . 1 holds
p1 ^ p2 is Path of G
let p1, p2 be Path of G; :: thesis: for vs1, vs2 being FinSequence of the carrier of G st rng p1 misses rng p2 & vs1 is_vertex_seq_of p1 & vs2 is_vertex_seq_of p2 & vs1 . (len vs1) = vs2 . 1 holds
p1 ^ p2 is Path of G
let vs1, vs2 be FinSequence of the carrier of G; :: thesis: ( rng p1 misses rng p2 & vs1 is_vertex_seq_of p1 & vs2 is_vertex_seq_of p2 & vs1 . (len vs1) = vs2 . 1 implies p1 ^ p2 is Path of G )
set c1 = p1;
set c2 = p2;
assume that
A1: rng p1 misses rng p2 and
A2: ( vs1 is_vertex_seq_of p1 & vs2 is_vertex_seq_of p2 & vs1 . (len vs1) = vs2 . 1 ) ; :: thesis: p1 ^ p2 is Path of G
reconsider c = p1 ^ p2 as Chain of G by A2, GRAPH_2:43;

now :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len c holds
not c . n = c . m

let n, m be Nat; :: thesis: ( 1 <= n & n < m & m <= len c implies not c . n = c . m )
assume that
A3: 1 <= n and
A4: n < m and
A5: m <= len c and
A6: c . n = c . m ; :: thesis: contradiction
1 <= m by A3, A4, XXREAL_0:2;
then A7: m in dom c by A5, FINSEQ_3:25;
n <= len c by A4, A5, XXREAL_0:2;
then A8: n in dom c by A3, FINSEQ_3:25;

per cases ( ( n in dom p1 & m in dom p1 ) or ( n in dom p1 & ex m2 being Nat st
( m2 in dom p2 & m = (len p1) + m2 ) ) or ( m in dom p1 & ex n2 being Nat st
( n2 in dom p2 & n = (len p1) + n2 ) ) or ( ex n2 being Nat st
( n2 in dom p2 & n = (len p1) + n2 ) & ex m2 being Nat st
( m2 in dom p2 & m = (len p1) + m2 ) ) ) by A8, A7, FINSEQ_1:25;

suppose A9: ( n in dom p1 & m in dom p1 ) ; :: thesis: contradiction

then p1 . n = c . n by FINSEQ_1:def 7
.= p1 . m by A6, A9, FINSEQ_1:def 7 ;
hence contradiction by A4, A9, FUNCT_1:def 4; :: thesis: verum

end;

suppose A10: ( n in dom p1 & ex m2 being Nat st
( m2 in dom p2 & m = (len p1) + m2 ) ) ; :: thesis: contradiction

then A11: p1 . n in rng p1 by FUNCT_1:def 3;
consider m2 being Nat such that
A12: m2 in dom p2 and
A13: m = (len p1) + m2 by A10;
A14: p2 . m2 in rng p2 by A12, FUNCT_1:def 3;
p1 . n = c . n by A10, FINSEQ_1:def 7
.= p2 . m2 by A6, A12, A13, FINSEQ_1:def 7 ;
hence contradiction by A1, A11, A14, XBOOLE_0:3; :: thesis: verum

end;

suppose A15: ( m in dom p1 & ex n2 being Nat st
( n2 in dom p2 & n = (len p1) + n2 ) ) ; :: thesis: contradiction

then consider n2 being Nat such that
n2 in dom p2 and
A16: n = (len p1) + n2 ;
m <= len p1 by A15, FINSEQ_3:25;
then (len p1) + n2 < len p1 by A4, A16, XXREAL_0:2;
hence contradiction by NAT_1:11; :: thesis: verum

end;

suppose A17: ( ex n2 being Nat st
( n2 in dom p2 & n = (len p1) + n2 ) & ex m2 being Nat st
( m2 in dom p2 & m = (len p1) + m2 ) ) ; :: thesis: contradiction

then consider n2 being Nat such that
A18: ( n2 in dom p2 & n = (len p1) + n2 ) ;
consider m2 being Nat such that
A19: ( m2 in dom p2 & m = (len p1) + m2 ) by A17;
p2 . n2 = c . n by A18, FINSEQ_1:def 7
.= p2 . m2 by A6, A19, FINSEQ_1:def 7 ;
hence contradiction by A4, A19, A18, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

hence p1 ^ p2 is Path of G by GRAPH_1:def 16; :: thesis: verum