set W = W1 ^' W2;
set lenW = len (W1 ^' W2);
hereby :: thesis: ( ( 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() ; :: 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 ;
then A6: (W1 ^' W2) . n = W1 . n by ;
(n + 2) - 1 <= (len W1) - 0 by ;
then A7: (W1 ^' W2) . (n + 1) = W1 . (n + 1) by ;
A8: (W1 ^' W2) . (n + 2) = W1 . (n + 2) by ;
n < len W1 by ;
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 ;
reconsider k = k as even Element of NAT by ;
k <> 0 by ;
then 0 + 1 < k + 1 by XREAL_1:8;
then A12: 1 <= k by NAT_1:13;
n + 1 < (len (W1 ^' W2)) + 1 by ;
then n + 1 < (len W1) + (len W2) by ;
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 ;
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 ;
(1 + 1) + 0 < (len W2) + 1 by ;
then A19: 1 < len W2 by XREAL_1:6;
then (W1 ^' W2) . (n + 1) = W2 . (1 + 1) by ;
hence (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G by ; :: 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 ;
then reconsider k2 = k - two as even Element of NAT by ;
(2 + (len W1)) - (len W1) < (k + (len W1)) - (len W1) by ;
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 ;
then A24: W2 . (kaa1 + 1) = (W1 ^' W2) . ((len W1) + kaa1) by
.= (W1 ^' W2) . (n + 1) by A11 ;
kaa1 < kaa1 + 1 by NAT_1:19;
then A25: kaa1 < len W2 by ;
kaa1 + 2 = k + 1 ;
then A26: W2 . (kaa1 + 2) = (W1 ^' W2) . (n + 2) by ;
k2 < k2 + (1 + 1) by NAT_1:16;
then A27: k2 < len W2 by ;
n + 2 = ((len W1) + k2) + 2 by A11;
then (W1 ^' W2) . n = W2 . (k2 + 1) by ;
hence (W1 ^' W2) . (n + 1) Joins (W1 ^' W2) . n,(W1 ^' W2) . (n + 2),G by ; :: 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 ;
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 ; :: thesis: verum
end;
thus ( ( not W1 .last() = W2 .first() implies W1 is Walk of G ) & ( for b1 being Walk of G holds verum ) ) ; :: thesis: verum