let G be _Graph; 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; 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 ; ( 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
; (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 ( 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))) )
;
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)) . xlet x be
Nat;
( 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)))
;
((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,o)) . xthen 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 ((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,o)) . xper cases
( x <= len (W .cut (m,n)) or x > len (W .cut (m,n)) )
;
suppose A15:
x <= len (W .cut (m,n))
;
((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,o)) . xthen 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
;
verum end; suppose
x > len (W .cut (m,n))
;
((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,o)) . xthen 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;
verum end; end; end; hence
((W .cut (m,n)) .append (W .cut (n,o))) . x = (W .cut (m,o)) . x
;
verum end;
hence
(W .cut (m,n)) .append (W .cut (n,o)) = W .cut (m,o)
by FINSEQ_2:9; verum