set W = W1 .append W2;
now
per cases ( W1 .last() = W2 .first() or W1 .last() <> W2 .first() ) ;
suppose A1: W1 .last() = W2 .first() ; :: thesis: W1 .append W2 is directed
now
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 HEYTING3:1;
then A3: n in dom (W1 .append W2) by A2, FINSEQ_3:27;
now
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: (W1 .append W2) . n = W1 . n by Lm12;
A6: ( 1 <= n & n <= len W1 ) by A4, FINSEQ_3:27;
now
per cases ( n < len W1 or n = len W1 ) by A6, 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 + 1 in dom W1 & n + 2 in dom W1 ) by Lm3;
then ( (W1 .append W2) . (n + 1) = W1 . (n + 1) & (W1 .append W2) . (n + 2) = W1 . (n + 2) ) by Lm12;
hence (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G by A5, A7, Lm51; :: thesis: verum
end;
suppose A8: n = len W1 ; :: thesis: (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G
then A9: ( 0 < len W2 & n = (len W1) + 0 ) ;
n + 1 < (len (W1 .append W2)) + 1 by A2, XREAL_1:10;
then 1 + n < (len W2) + n by A1, A8, Lm9;
then A10: ( 1 < len W2 & n + 1 = (len W1) + 1 ) by A8, XREAL_1:8;
then A11: (W1 .append W2) . (n + 1) = W2 . (1 + 1) by A1, Lm13;
1 + 1 <= len W2 by A10, NAT_1:13;
then ( 2 * 1 < len W2 & n + 2 = (len W1) + 2 ) by A8, XXREAL_0:1;
then A12: (W1 .append W2) . (n + 2) = W2 . (2 + 1) by A1, Lm13;
W2 . (((2 * 0 ) + 1) + 1) DJoins W2 . ((2 * 0 ) + 1),W2 . (((2 * 0 ) + 1) + 2),G by A10, Lm51;
hence (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G by A1, A9, A11, A12, 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
A13: ( k < len W2 & n = (len W1) + k ) ;
k is even by A13;
then reconsider k = k as even Element of NAT ;
A14: (W1 .append W2) . n = W2 . (k + 1) by A1, A13, Lm13;
n + 1 < (len (W1 .append W2)) + 1 by A2, XREAL_1:10;
then 1 + (k + (len W1)) < (len W2) + (len W1) by A1, A13, Lm9;
then A15: ((k + 1) + (len W1)) - (len W1) < ((len W2) + (len W1)) - (len W1) by XREAL_1:16;
then (k + 1) + 1 <= len W2 by NAT_1:13;
then A16: (k + 1) + 1 < len W2 by XXREAL_0:1;
A17: (n + 1) + 1 = (len W1) + ((k + 1) + 1) by A13;
A18: (W1 .append W2) . (n + 1) = W2 . ((k + 1) + 1) by A1, A13, A15, Lm13;
W2 . ((k + 1) + (1 + 1)) = W2 . (((k + 1) + 1) + 1)
.= (W1 .append W2) . (n + (1 + 1)) by A1, A16, A17, Lm13 ;
hence (W1 .append W2) . (n + 1) DJoins (W1 .append W2) . n,(W1 .append W2) . (n + 2),G by A14, A15, A18, 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