let G be _Graph; :: thesis:
let P1, P2 be Path of G; :: thesis:
assume that
A1: P1 .last() = P2 .first() and
A2: not P1 is closed and
A3: not P2 is closed and
A4: P1 .edges() misses P2 .edges() and
A5: ( P1 .first() in P2 .vertices() implies P1 .first() = P2 .last() ) and
A6: (P1 .vertices() ) /\ (P2 .vertices() ) c= {(P1 .first() ),(P1 .last() )} ; :: thesis:
set P = P1 .append P2;
thus P1 .append P2 is Trail-like by A1, A4, Th16; :: according to GLIB_001:def 28 :: thesis:
let m, n be odd Element of NAT ; :: thesis:
assume that
A7: m < n and
A8: n <= len (P1 .append P2) and
A9: (P1 .append P2) . m = (P1 .append P2) . n and
A10: ( m <> 1 or n <> len (P1 .append P2) ) ; :: thesis:
1 <= n by HEYTING3:1;
then A11: n in dom (P1 .append P2) by A8, FINSEQ_3:27;
A12: ( 1 <= m & m <= len (P1 .append P2) ) by A7, A8, HEYTING3:1, XXREAL_0:2;
then A13: m in dom (P1 .append P2) by FINSEQ_3:27;

per cases by A11, GLIB_001:35;

suppose ex k being Element of NAT st
( k < len P2 & n = (len P1) + k ) ; :: thesis:

then consider k being Element of NAT such that
A14: k < len P2 and
A15: n = (len P1) + k ;
A16: (P1 .append P2) . n = P2 . (k + 1) by A1, A14, A15, GLIB_001:34;
reconsider k = k as even Element of NAT by A15;
A17: k + 1 <= len P2 by A14, NAT_1:13;
then A18: P2 . (k + 1) in P2 .vertices() by GLIB_001:88;

per cases by A13, GLIB_001:35;

suppose ex k being Element of NAT st
( k < len P2 & m = (len P1) + k ) ; :: thesis:

then consider l being Element of NAT such that
A19: l < len P2 and
A20: m = (len P1) + l ;
A21: (P1 .append P2) . m = P2 . (l + 1) by A1, A19, A20, GLIB_001:34;
l < k by A7, A15, A20, XREAL_1:8;
then A22: l + 1 < k + 1 by XREAL_1:8;
reconsider l = l as even Element of NAT by A20;
not l + 1 is even ;
then ( P2 .first() = P2 . (l + 1) & P2 .last() = P2 . (k + 1) ) by A9, A16, A17, A21, A22, GLIB_001:def 28;
hence contradiction by A3, A9, A16, A21, GLIB_001:def 24; :: thesis:

end;

suppose A23: m in dom P1 ; :: thesis:

then A24: P1 . m = (P1 .append P2) . m by GLIB_001:33;
A25: m <= len P1 by A23, FINSEQ_3:27;
then A26: P1 . m in P1 .vertices() by GLIB_001:88;
set x = P1 . m;
A27: P1 . m in (P1 .vertices() ) /\ (P2 .vertices() ) by A9, A16, A18, A24, A26, XBOOLE_0:def 4;

per cases by A6, A27, TARSKI:def 2;

suppose A28: P1 . m = P1 .last() ; :: thesis:

A29: now

assume m < len P1 ; :: thesis:
then P1 .first() = P1 . m by A28, GLIB_001:def 28;
hence contradiction by A2, A28, GLIB_001:def 24; :: thesis:

end;

A30: now

assume (2 * 0 ) + 1 < k + 1 ; :: thesis:
then P2 .first() = P2 .last() by A1, A9, A16, A17, A24, A28, GLIB_001:def 28;
hence contradiction by A3, GLIB_001:def 24; :: thesis:

end;

1 <= k + 1 by NAT_1:11;
then 1 = k + 1 by A30, XXREAL_0:1;
hence contradiction by A7, A15, A29; :: thesis:

end;

suppose A31: P1 . m = P1 .first() ; :: thesis:

then A32: P1 . m = P1 . ((2 * 0 ) + 1) ;

A33: now

assume m <> 1 ; :: thesis:
then 1 < m by A12, XXREAL_0:1;
then P1 . m = P1 .last() by A25, A32, GLIB_001:def 28;
hence contradiction by A2, A31, GLIB_001:def 24; :: thesis:

end;

A34: P2 . (k + 1) = P2 .last() by A5, A9, A16, A18, A23, A31, GLIB_001:33;

assume k + 1 = len P2 ; :: thesis:
then (len (P1 .append P2)) + 1 = (len P1) + (k + 1) by A1, GLIB_001:29;
hence contradiction by A10, A15, A33; :: thesis:

end;

then k + 1 < len P2 by A17, XXREAL_0:1;
then P2 .first() = P2 .last() by A34, GLIB_001:def 28;
hence contradiction by A3, GLIB_001:def 24; :: thesis:

end;

suppose A35: n in dom P1 ; :: thesis:

then A36: ( 1 <= n & n <= len P1 ) by FINSEQ_3:27;
then ( 1 <= m & m <= len P1 ) by A7, HEYTING3:1, XXREAL_0:2;
then m in dom P1 by FINSEQ_3:27;
then A37: P1 . m = (P1 .append P2) . m by GLIB_001:33
.= P1 . n by A9, A35, GLIB_001:33 ;
then ( m = 1 & n = len P1 ) by A7, A36, GLIB_001:def 28;
then P1 .first() = P1 .last() by A37;
hence contradiction by A2, GLIB_001:def 24; :: thesis:

end;