set W = W1 ^' W2;
set lenW = len (W1 ^' W2);

hereby :: thesis: ( ( not W1 .last() = W2 .first() implies W1 is Walk of G ) & ( for b₁ being Walk of G holds verum ) )

assume A1: W1 .last() = W2 .first() ; :: thesis: W1 ^' W2 is Walk of G

A2: now :: thesis: for n being odd Element of NAT st n < len (W1 ^' W2) holds
(W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G

let n be odd Element of NAT ; :: thesis: ( n < len (W1 ^' W2) implies (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G )
assume A3: n < len (W1 ^' W2) ; :: thesis: (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G
set v1 = (W1 ^' W2) . n;
set v2 = (W1 ^' W2) . (n + 2);
set e = (W1 ^' W2) . (n + 1);

now :: thesis: (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G

per cases ( n + 2 <= len W1 or len W1 < n + 2 ) ;

suppose A4: n + 2 <= len W1 ; :: thesis: (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G

A5: 1 <= n by ABIAN:12;
(n + 2) - 2 <= (len W1) - 0 by A4, XREAL_1:13;
then A6: (W1 ^' W2) . n = W1 . n by A5, FINSEQ_6:140;
(n + 2) - 1 <= (len W1) - 0 by A4, XREAL_1:13;
then A7: (W1 ^' W2) . (n + 1) = W1 . (n + 1) by FINSEQ_6:140, NAT_1:12;
A8: (W1 ^' W2) . (n + 2) = W1 . (n + 2) by A4, FINSEQ_6:140, NAT_1:12;
n < len W1 by A4, NAT_1:16, XXREAL_0:2;
hence (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G by A6, A7, A8, Def3; :: thesis: verum

end;

suppose A9: len W1 < n + 2 ; :: thesis: (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G

then (len W1) + 1 <= n + 2 by NAT_1:13;
then (len W1) + 1 < (n + 1) + 1 by XXREAL_0:1;
then len W1 < n + 1 by XREAL_1:6;
then A10: len W1 <= n by NAT_1:13;
consider k being Nat such that
A11: n + 2 = (len W1) + k by A9, NAT_1:10;
reconsider k = k as even Element of NAT by A11, ORDINAL1:def 12;
k <> 0 by A9, A11;
then 0 + 1 < k + 1 by XREAL_1:8;
then A12: 1 <= k by NAT_1:13;
n + 1 < (len (W1 ^' W2)) + 1 by A3, XREAL_1:8;
then n + 1 < (len W1) + (len W2) by CARD_1:27, FINSEQ_6:139;
then (n + 1) + 1 < ((len W1) + (len W2)) + 1 by XREAL_1:8;
then A13: k + (len W1) < (len W1) + ((len W2) + 1) by A11;
then k < (len W2) + 1 by XREAL_1:6;
then A14: k <= len W2 by NAT_1:13;
then A15: k < len W2 by XXREAL_0:1;
then A16: (W1 ^' W2) . (n + 2) = W2 . (k + 1) by A11, A12, FINSEQ_6:141;

now :: thesis: (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G

per cases ( n = len W1 or len W1 <> n ) ;

suppose A17: n = len W1 ; :: thesis: (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G

1 <= n by ABIAN:12;
then A18: (W1 ^' W2) . n = W1 . (len W1) by A17, FINSEQ_6:140;
(1 + 1) + 0 < (len W2) + 1 by A11, A13, A17, XREAL_1:6;
then A19: 1 < len W2 by XREAL_1:6;
then (W1 ^' W2) . (n + 1) = W2 . (1 + 1) by A17, FINSEQ_6:141;
hence (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G by A1, A11, A16, A17, A18, A19, Def3, JORDAN12:2; :: thesis: verum

end;

suppose A20: len W1 <> n ; :: thesis: (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G

reconsider two = 2 * 1 as even Element of NAT ;
A21: len W1 < n by A10, A20, XXREAL_0:1;
then reconsider k2 = k - two as even Element of NAT by A11, INT_1:5, XREAL_1:8;
(2 + (len W1)) - (len W1) < (k + (len W1)) - (len W1) by A11, A21, XREAL_1:8;
then (1 + 1) - 1 < ((k2 + 1) + 1) - 1 by XREAL_1:14;
then A22: 1 <= k2 by NAT_1:13;
set kaa1 = k2 + 1;
reconsider kaa1 = k2 + 1 as odd Element of NAT ;
A23: 1 <= k2 + 1 by NAT_1:12;
(kaa1 + 1) - 1 < (len W2) - 0 by A14, XREAL_1:15;
then A24: W2 . (kaa1 + 1) = (W1 ^' W2) . ((len W1) + kaa1) by A23, FINSEQ_6:141
.= (W1 ^' W2) . (n + 1) by A11 ;
kaa1 < kaa1 + 1 by NAT_1:19;
then A25: kaa1 < len W2 by A14, XXREAL_0:2;
kaa1 + 2 = k + 1 ;
then A26: W2 . (kaa1 + 2) = (W1 ^' W2) . (n + 2) by A11, A12, A15, FINSEQ_6:141;
k2 < k2 + (1 + 1) by NAT_1:16;
then A27: k2 < len W2 by A14, XXREAL_0:2;
n + 2 = ((len W1) + k2) + 2 by A11;
then (W1 ^' W2) . n = W2 . (k2 + 1) by A22, A27, FINSEQ_6:141;
hence (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G by A26, A25, A24, Def3; :: thesis: verum

end;

end;

end;

hence (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G ; :: thesis: verum

end;

end;

end;

hence (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G ; :: thesis: verum

end;

A28: now :: thesis: not len (W1 ^' W2) is even

assume len (W1 ^' W2) is even ; :: thesis: contradiction
then reconsider lenW = len (W1 ^' W2) as even Element of NAT ;
lenW + 1 = (len W1) + (len W2) by CARD_1:27, FINSEQ_6:139;
hence contradiction ; :: thesis: verum

end;

1 <= len W1 by ABIAN:12;
then (W1 ^' W2) . 1 = W1 .first() by FINSEQ_6:140;
hence W1 ^' W2 is Walk of G by A28, A2, Def3; :: thesis: verum

end;

thus ( ( not W1 .last() = W2 .first() implies W1 is Walk of G ) & ( for b₁ being Walk of G holds verum ) ) ; :: thesis: verum