let G be _Graph; :: thesis: for W1, W2 being Trail of G st W1 .last() = W2 .first() & W1 .edges() misses W2 .edges() holds
W1 .append W2 is Trail-like
let W1, W2 be Trail of G; :: thesis: ( W1 .last() = W2 .first() & W1 .edges() misses W2 .edges() implies W1 .append W2 is Trail-like )
assume that
A1: W1 .last() = W2 .first() and
A2: W1 .edges() misses W2 .edges() ; :: thesis: W1 .append W2 is Trail-like
set W = W1 .append W2;

now :: thesis: for m, n being even Element of NAT st 1 <= m & m < n & n <= len (W1 .append W2) holds
(W1 .append W2) . m <> (W1 .append W2) . n

let m, n be even Element of NAT ; :: thesis: ( 1 <= m & m < n & n <= len (W1 .append W2) implies (W1 .append W2) . b₁ <> (W1 .append W2) . b₂ )
assume that
A3: 1 <= m and
A4: m < n and
A5: n <= len (W1 .append W2) ; :: thesis: (W1 .append W2) . b₁ <> (W1 .append W2) . b₂
1 <= n by A3, A4, XXREAL_0:2;
then A6: n in dom (W1 .append W2) by A5, FINSEQ_3:25;
m <= len (W1 .append W2) by A4, A5, XXREAL_0:2;
then A7: m in dom (W1 .append W2) by A3, FINSEQ_3:25;

per cases ( n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) ) by A6, GLIB_001:34;

suppose A8: n in dom W1 ; :: thesis: (W1 .append W2) . b₁ <> (W1 .append W2) . b₂

then A9: n <= len W1 by FINSEQ_3:25;
then m <= len W1 by A4, XXREAL_0:2;
then m in dom W1 by A3, FINSEQ_3:25;
then A10: W1 . m = (W1 .append W2) . m by GLIB_001:32;
W1 . m <> W1 . n by A3, A4, A9, GLIB_001:138;
hence (W1 .append W2) . m <> (W1 .append W2) . n by A8, A10, GLIB_001:32; :: thesis: verum

end;

suppose ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) ; :: thesis: (W1 .append W2) . b₁ <> (W1 .append W2) . b₂

then consider k being Element of NAT such that
A11: k < len W2 and
A12: n = (len W1) + k ;
reconsider k = k as odd Element of NAT by A12;
A13: (W1 .append W2) . n = W2 . (k + 1) by A1, A11, A12, GLIB_001:33;
A14: k + 1 <= len W2 by A11, NAT_1:13;
1 <= k + 1 by NAT_1:11;
then A15: W2 . (k + 1) in W2 .edges() by A14, GLIB_001:99;

per cases ( m in dom W1 or ex l being Element of NAT st
( l < len W2 & m = (len W1) + l ) ) by A7, GLIB_001:34;

suppose A16: m in dom W1 ; :: thesis: (W1 .append W2) . b₁ <> (W1 .append W2) . b₂

then ( 1 <= m & m <= len W1 ) by FINSEQ_3:25;
then A17: W1 . m in W1 .edges() by GLIB_001:99;
(W1 .append W2) . m = W1 . m by A16, GLIB_001:32;
hence (W1 .append W2) . m <> (W1 .append W2) . n by A2, A13, A15, A17, XBOOLE_0:3; :: thesis: verum

end;

suppose ex l being Element of NAT st
( l < len W2 & m = (len W1) + l ) ; :: thesis: (W1 .append W2) . b₁ <> (W1 .append W2) . b₂

then consider l being Element of NAT such that
A18: l < len W2 and
A19: m = (len W1) + l ;
reconsider l = l as odd Element of NAT by A19;
l < k by A4, A12, A19, XREAL_1:6;
then A20: ( 1 <= l + 1 & l + 1 < k + 1 ) by NAT_1:11, XREAL_1:6;
(W1 .append W2) . m = W2 . (l + 1) by A1, A18, A19, GLIB_001:33;
hence (W1 .append W2) . m <> (W1 .append W2) . n by A13, A14, A20, GLIB_001:138; :: thesis: verum

end;

end;

end;

end;

end;

hence W1 .append W2 is Trail-like by GLIB_001:138; :: thesis: verum