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 and
A3: vs2 is_vertex_seq_of p2 and
A4: vs1 . (len vs1) = vs2 . 1 ; :: thesis: p1 ^ p2 is Path of G
reconsider c = p1 ^ p2 as Chain of G by A2, A3, A4, GRAPH_2:46;

now

let n, m be Element of NAT ; :: thesis: ( 1 <= n & n < m & m <= len c implies not c . n = c . m )
assume that
A5: ( 1 <= n & n < m & m <= len c ) and
A6: c . n = c . m ; :: thesis: contradiction
( 1 <= m & n <= len c ) by A5, XXREAL_0:2;
then A7: ( n in dom c & m in dom c ) by A5, FINSEQ_3:27;

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 A7, FINSEQ_1:38;

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

then p1 . n = c . n by FINSEQ_1:def 7
.= p1 . m by A6, A8, FINSEQ_1:def 7 ;
hence contradiction by A5, A8, FUNCT_1:def 8; :: thesis: verum

end;

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

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

end;

suppose A12: ( 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
A13: ( n2 in dom p2 & n = (len p1) + n2 ) ;
m <= len p1 by A12, FINSEQ_3:27;
then (len p1) + n2 < len p1 by A5, A13, XXREAL_0:2;
hence contradiction by NAT_1:11; :: thesis: verum

end;

suppose A14: ( 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 m2 being Nat such that
A15: ( m2 in dom p2 & m = (len p1) + m2 ) ;
consider n2 being Nat such that
A16: ( n2 in dom p2 & n = (len p1) + n2 ) by A14;
p2 . n2 = c . n by A16, FINSEQ_1:def 7
.= p2 . m2 by A6, A15, FINSEQ_1:def 7 ;
hence contradiction by A5, A15, A16, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

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