set W = W1 ^' W2;
set lenW = len (W1 ^' W2);
hereby ( ( not W1 .last() = W2 .first() implies W1 is Walk of G ) & ( for b1 being Walk of G holds verum ) )
assume A1:
W1 .last() = W2 .first()
;
W1 ^' W2 is Walk of GA2:
now 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),Glet n be
odd Element of
NAT ;
( n < len (W1 ^' W2) implies (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G )assume A3:
n < len (W1 ^' W2)
;
(W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),Gset v1 =
(W1 ^' W2) . n;
set v2 =
(W1 ^' W2) . (n + 2);
set e =
(W1 ^' W2) . (n + 1);
now (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),Gper cases
( n + 2 <= len W1 or len W1 < n + 2 )
;
suppose A4:
n + 2
<= len W1
;
(W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),GA5:
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;
verum end; suppose A9:
len W1 < n + 2
;
(W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),Gthen
(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 (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),Gper cases
( n = len W1 or len W1 <> n )
;
suppose A17:
n = len W1
;
(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;
verum end; suppose A20:
len W1 <> n
;
(W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),Greconsider 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;
verum end; end; end; hence
(W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,
(W1 ^' W2) . (n + 2),
G
;
verum end; end; end; hence
(W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,
(W1 ^' W2) . (n + 2),
G
;
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;
verum
end;
thus
( ( not W1 .last() = W2 .first() implies W1 is Walk of G ) & ( for b1 being Walk of G holds verum ) )
; verum