let G be _Graph; :: thesis: for W being Walk of G
for m, n, o being odd Element of NAT st m <= n & n <= o & o <= len W holds
(W .cut (m,n)) .append (W .cut (n,o)) = W .cut (m,o)
let W be Walk of G; :: thesis: for m, n, o being odd Element of NAT st m <= n & n <= o & o <= len W holds
(W .cut (m,n)) .append (W .cut (n,o)) = W .cut (m,o)
let m, n, o be odd Element of NAT ; :: thesis: ( m <= n & n <= o & o <= len W implies (W .cut (m,n)) .append (W .cut (n,o)) = W .cut (m,o) )
assume that
A1: m <= n and
A2: n <= o and
A3: o <= len W ; :: thesis: (W .cut (m,n)) .append (W .cut (n,o)) = W .cut (m,o)
set W1 = W .cut (m,n);
set W2 = W .cut (n,o);
set W3 = W .cut (m,o);
set W4 = (W .cut (m,n)) .append (W .cut (n,o));
A4: n <= len W by A2, A3, XXREAL_0:2;
A5: m <= o by A1, A2, XXREAL_0:2;
now :: thesis: ( len ((W .cut (m,n)) .append (W .cut (n,o))) = len ((W .cut (m,n)) .append (W .cut (n,o))) & len (W .cut (m,o)) = len ((W .cut (m,n)) .append (W .cut (n,o))) & ( for x being Nat st x in dom ((W .cut (m,n)) .append (W .cut (n,o))) holds
((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,o)) . x ) )
A6: (len (W .cut (m,o))) + m = o + 1 by A3, A5, Lm15;
A7: (W .cut (m,n)) .last() = W . n by A1, A4, Lm16
.= (W .cut (n,o)) .first() by A2, A3, Lm16 ;
A8: (len (W .cut (m,n))) + m = n + 1 by A1, A4, Lm15;
A9: (len (W .cut (n,o))) + n = o + 1 by A2, A3, Lm15;
then ((len (W .cut (m,n))) + (len (W .cut (n,o)))) + m = (1 + (len (W .cut (m,o)))) + m by A8, A6;
then A10: (len ((W .cut (m,n)) .append (W .cut (n,o)))) + 1 = (len (W .cut (m,o))) + 1 by A7, Lm9;
hence ( len ((W .cut (m,n)) .append (W .cut (n,o))) = len ((W .cut (m,n)) .append (W .cut (n,o))) & len (W .cut (m,o)) = len ((W .cut (m,n)) .append (W .cut (n,o))) ) ; :: thesis: for x being Nat st x in dom ((W .cut (m,n)) .append (W .cut (n,o))) holds
((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,o)) . x
let x be Nat; :: thesis: ( x in dom ((W .cut (m,n)) .append (W .cut (n,o))) implies ((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,o)) . x )
assume A11: x in dom ((W .cut (m,n)) .append (W .cut (n,o))) ; :: thesis: ((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,o)) . x
then A12: 1 <= x by FINSEQ_3:25;
then reconsider xaa1 = x - 1 as Element of NAT by INT_1:5;
A13: x <= len ((W .cut (m,n)) .append (W .cut (n,o))) by A11, FINSEQ_3:25;
then xaa1 < (len ((W .cut (m,n)) .append (W .cut (n,o)))) - 0 by XREAL_1:15;
then A14: (W .cut (m,o)) . (xaa1 + 1) = W . (m + xaa1) by A3, A5, A10, Lm15;
now :: thesis: ((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,o)) . x
per cases ( x <= len (W .cut (m,n)) or x > len (W .cut (m,n)) ) ;
suppose A15: x <= len (W .cut (m,n)) ; :: thesis: ((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,o)) . x
then A16: xaa1 < (len (W .cut (m,n))) - 0 by XREAL_1:15;
x in dom (W .cut (m,n)) by A12, A15, FINSEQ_3:25;
hence ((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,n)) . (xaa1 + 1) by Lm12
.= (W .cut (m,o)) . x by A1, A4, A14, A16, Lm15 ;
:: thesis: verum
end;
suppose x > len (W .cut (m,n)) ; :: thesis: ((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,o)) . x
then consider k being Nat such that
A17: (len (W .cut (m,n))) + k = x by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
((len (W .cut (m,n))) + k) + 1 <= (len (W .cut (m,o))) + 1 by A10, A13, A17, XREAL_1:7;
then ((k + 1) + (len (W .cut (m,n)))) - (len (W .cut (m,n))) <= ((len (W .cut (n,o))) + (len (W .cut (m,n)))) - (len (W .cut (m,n))) by A8, A9, A6, XREAL_1:13;
then A18: (k + 1) - 1 < ((len (W .cut (n,o))) + 1) - 1 by NAT_1:13;
then ((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (n,o)) . (k + 1) by A7, A17, Lm13
.= W . (n + k) by A2, A3, A18, Lm15 ;
hence ((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,o)) . x by A8, A14, A17; :: thesis: verum
end;
end;
end;
hence ((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,o)) . x ; :: thesis: verum
end;
hence (W .cut (m,n)) .append (W .cut (n,o)) = W .cut (m,o) by FINSEQ_2:9; :: thesis: verum