set W = W1 .append W2;
now :: thesis: W1 .append W2 is directed
per cases ( W1 .last() = W2 .first() or W1 .last() <> W2 .first() ) ;
suppose A1: W1 .last() = W2 .first() ; :: thesis: W1 .append W2 is directed
now :: thesis: for n being odd Element of NAT st n < len (W1 .append W2) holds
(W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G
let n be odd Element of NAT ; :: thesis: ( n < len (W1 .append W2) implies (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G )
assume A2: n < len (W1 .append W2) ; :: thesis: (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G
1 <= n by ABIAN:12;
then A3: n in dom (W1 .append W2) by A2, FINSEQ_3:25;
now :: thesis: (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G
per cases ( n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) ) by A3, Lm14;
suppose A4: n in dom W1 ; :: thesis: (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G
then A5: n <= len W1 by FINSEQ_3:25;
A6: (W1 .append W2) . n = W1 . n by A4, Lm12;
now :: thesis: (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G
per cases ( n < len W1 or n = len W1 ) by A5, XXREAL_0:1;
suppose A7: n < len W1 ; :: thesis: (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G
then n + 2 in dom W1 by Lm3;
then A8: (W1 .append W2) . (n + 2) = W1 . (n + 2) by Lm12;
n + 1 in dom W1 by A7, Lm3;
then (W1 .append W2) . (n + 1) = W1 . (n + 1) by Lm12;
hence (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G by A6, A7, A8, Lm51; :: thesis: verum
end;
suppose A9: n = len W1 ; :: thesis: (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G
n + 1 < (len (W1 .append W2)) + 1 by A2, XREAL_1:8;
then 1 + n < (len W2) + n by A1, A9, Lm9;
then A10: 1 < len W2 by XREAL_1:6;
then A11: W2 . (((2 * 0) + 1) + 1) DJoins W2 . ((2 * 0) + 1),W2 . (((2 * 0) + 1) + 2),G by Lm51;
A12: n = (len W1) + 0 by A9;
A13: 0 < len W2 ;
1 + 1 <= len W2 by A10, NAT_1:13;
then 2 * 1 < len W2 by XXREAL_0:1;
then A14: (W1 .append W2) . (n + 2) = W2 . (2 + 1) by A1, A9, Lm13;
(W1 .append W2) . (n + 1) = W2 . (1 + 1) by A1, A9, A10, Lm13;
hence (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G by A1, A13, A12, A14, A11, Lm13; :: thesis: verum
end;
end;
end;
hence (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G ; :: thesis: verum
end;
suppose ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) ; :: thesis: (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G
then consider k being Element of NAT such that
A15: k < len W2 and
A16: n = (len W1) + k ;
reconsider k = k as even Element of NAT by A16;
A17: (W1 .append W2) . n = W2 . (k + 1) by A1, A15, A16, Lm13;
n + 1 < (len (W1 .append W2)) + 1 by A2, XREAL_1:8;
then 1 + (k + (len W1)) < (len W2) + (len W1) by A1, A16, Lm9;
then A18: ((k + 1) + (len W1)) - (len W1) < ((len W2) + (len W1)) - (len W1) by XREAL_1:14;
then (k + 1) + 1 <= len W2 by NAT_1:13;
then A19: (k + 1) + 1 < len W2 by XXREAL_0:1;
A20: (n + 1) + 1 = (len W1) + ((k + 1) + 1) by A16;
A21: W2 . ((k + 1) + (1 + 1)) = W2 . (((k + 1) + 1) + 1)
.= (W1 .append W2) . (n + (1 + 1)) by A1, A19, A20, Lm13 ;
(W1 .append W2) . (n + 1) = W2 . ((k + 1) + 1) by A1, A16, A18, Lm13;
hence (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G by A17, A18, A21, Lm51; :: thesis: verum
end;
end;
end;
hence (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G ; :: thesis: verum
end;
hence W1 .append W2 is directed by Lm51; :: thesis: verum
end;
end;
end;
hence W1 .append W2 is directed ; :: thesis: verum