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:
thus P1 .append P2 is Trail-like by A1, A4, Th17; :: according to GLIB_001:def 28 :: thesis:
set P = P1 .append P2;
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:
A11: 1 <= m by ABIAN:12;
1 <= n by ABIAN:12;
then A12: n in dom (P1 .append P2) by A8, FINSEQ_3:27;
m <= len (P1 .append P2) by A7, A8, XXREAL_0:2;
then A13: m in dom (P1 .append P2) by A11, FINSEQ_3:27;

per cases by A12, 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 A23: P2 .last() = P2 . (k + 1) by A9, A16, A17, A21, A22, GLIB_001:def 28;
P2 .first() = P2 . (l + 1) by A9, A16, A17, A21, A22, GLIB_001:def 28;
hence contradiction by A3, A9, A16, A21, A23, GLIB_001:def 24; :: thesis:

end;

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

set x = P1 . m;
A25: P1 . m = (P1 .append P2) . m by A24, GLIB_001:33;
A26: m <= len P1 by A24, FINSEQ_3:27;
then P1 . m in P1 .vertices() by GLIB_001:88;
then A27: P1 . m in (P1 .vertices()) /\ (P2 .vertices()) by A9, A16, A18, A25, 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, A25, 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 A11, XXREAL_0:1;
then P1 . m = P1 .last() by A26, A32, GLIB_001:def 28;
hence contradiction by A2, A31, GLIB_001:def 24; :: thesis:

end;

now

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 A34: k + 1 < len P2 by A17, XXREAL_0:1;
P2 . (k + 1) = P2 .last() by A5, A9, A16, A18, A24, A31, GLIB_001:33;
then P2 .first() = P2 .last() by A34, GLIB_001:def 28;
hence contradiction by A3, GLIB_001:def 24; :: thesis:

end;

end;

end;

end;

end;

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

then A36: n <= len P1 by FINSEQ_3:27;
then ( 1 <= m & m <= len P1 ) by A7, ABIAN:12, 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 by A7, A36, GLIB_001:def 28;
then P1 .first() = P1 .last() by A7, A36, A37, GLIB_001:def 28;
hence contradiction by A2, GLIB_001:def 24; :: thesis:

end;

end;