set W = W1 ^' W2;

set lenW = len (W1 ^' W2);

_{1} being Walk of G holds verum ) )
; :: thesis: verum

set lenW = len (W1 ^' W2);

hereby :: thesis: ( ( not W1 .last() = W2 .first() implies W1 is Walk of G ) & ( for b_{1} being Walk of G holds verum ) )

thus
( ( not W1 .last() = W2 .first() implies W1 is Walk of G ) & ( for bassume A1:
W1 .last() = W2 .first()
; :: thesis: W1 ^' W2 is Walk of G

then (W1 ^' W2) . 1 = W1 .first() by FINSEQ_6:140;

hence W1 ^' W2 is Walk of G by A28, A2, Def3; :: thesis: verum

end;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

(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);

end;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),Gend;

hence
(W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G
; :: thesis: verumper cases
( n + 2 <= len W1 or len W1 < n + 2 )
;

end;

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;(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

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;

end;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),Gend;

hence
(W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G
; :: thesis: verumper cases
( n = len W1 or len W1 <> n )
;

end;

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;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

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;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

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

1 <= len W1
by ABIAN:12;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;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

then (W1 ^' W2) . 1 = W1 .first() by FINSEQ_6:140;

hence W1 ^' W2 is Walk of G by A28, A2, Def3; :: thesis: verum