set W2 = W .remove (m,n);
A1: len (W .remove (m,n)) <= len W by Lm26;
now :: thesis: W .remove (m,n) is Path-like
per cases ( ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n ) or not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n ) ;
suppose A2: ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n ) ; :: thesis: W .remove (m,n) is Path-like
then reconsider m9 = m, n9 = n as odd Element of NAT ;
now :: thesis: for x, y being odd Element of NAT st x < y & y <= len (W .remove (m,n)) & (W .remove (m,n)) . x = (W .remove (m,n)) . y holds
( x = 1 & y = len (W .remove (m,n)) )
let x, y be odd Element of NAT ; :: thesis: ( x < y & y <= len (W .remove (m,n)) & (W .remove (m,n)) . x = (W .remove (m,n)) . y implies ( x = 1 & y = len (W .remove (m,n)) ) )
assume that
A3: x < y and
A4: y <= len (W .remove (m,n)) and
A5: (W .remove (m,n)) . x = (W .remove (m,n)) . y ; :: thesis: ( x = 1 & y = len (W .remove (m,n)) )
A6: 1 <= x by ABIAN:12;
x <= len (W .remove (m,n)) by ;
then A7: x in dom (W .remove (m,n)) by ;
1 <= y by ABIAN:12;
then A8: y in dom (W .remove (m,n)) by ;
A9: y <= len W by ;
now :: thesis: ( x = 1 & y = len (W .remove (m,n)) )
per cases ( x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) ) by A2, A7, Lm34;
suppose x in Seg m ; :: thesis: ( x = 1 & y = len (W .remove (m,n)) )
then A10: (W .remove (m,n)) . x = W . x by ;
now :: thesis: ( x = 1 & y = len (W .remove (m,n)) )
per cases ( y in Seg m or ( m <= y & y <= len (W .remove (m,n)) ) ) by A2, A8, Lm34;
suppose y in Seg m ; :: thesis: ( x = 1 & y = len (W .remove (m,n)) )
then A11: (W .remove (m,n)) . y = W . y by ;
then y = len W by A3, A5, A9, A10, Def28;
hence ( x = 1 & y = len (W .remove (m,n)) ) by ; :: thesis: verum
end;
suppose A12: ( m <= y & y <= len (W .remove (m,n)) ) ; :: thesis: ( x = 1 & y = len (W .remove (m,n)) )
then A13: (y - m) + n <= len W by ;
A14: (W .remove (m,n)) . y = W . ((y - m) + n) by ;
reconsider y2 = (y - m9) + n9 as odd Element of NAT by ;
(y - m) + n >= (y - m) + m by ;
then A15: x < y2 by ;
y2 <= len W by ;
then y2 = len W by A5, A10, A14, A15, Def28;
then (len (W .remove (m,n))) + n = ((y - m) + n) + m by
.= y + n ;
hence ( x = 1 & y = len (W .remove (m,n)) ) by A5, A10, A14, A13, A15, Def28; :: thesis: verum
end;
end;
end;
hence ( x = 1 & y = len (W .remove (m,n)) ) ; :: thesis: verum
end;
suppose A16: ( m <= x & x <= len (W .remove (m,n)) ) ; :: thesis: ( x = 1 & y = len (W .remove (m,n)) )
then reconsider x2 = (x - m9) + n9 as odd Element of NAT by ;
A17: (W .remove (m,n)) . x = W . ((x - m) + n) by ;
now :: thesis: ( x = 1 & y = len (W .remove (m,n)) )
per cases ( y in Seg m or ( m <= y & y <= len (W .remove (m,n)) ) ) by A2, A8, Lm34;
suppose y in Seg m ; :: thesis: ( x = 1 & y = len (W .remove (m,n)) )
then y <= m by FINSEQ_1:1;
hence ( x = 1 & y = len (W .remove (m,n)) ) by ; :: thesis: verum
end;
suppose A18: ( m <= y & y <= len (W .remove (m,n)) ) ; :: thesis: ( x = 1 & y = len (W .remove (m,n)) )
then reconsider y2 = (y - m9) + n9 as odd Element of NAT by ;
x + (n - m) < y + (n - m) by ;
then A19: x2 < y2 ;
reconsider xm4 = x - m as Element of NAT by ;
A20: 1 <= n9 by ABIAN:12;
A21: 1 <= m9 by ABIAN:12;
A22: (y - m) + n <= len W by ;
A23: (W .remove (m,n)) . y = W . ((y - m) + n) by ;
then y2 = len W by A5, A17, A22, A19, Def28;
then A24: (len (W .remove (m,n))) + n = ((y - m) + n) + m by
.= y + n ;
x2 = 1 by A5, A17, A23, A22, A19, Def28;
then x2 - n9 <= 1 - 1 by ;
then A25: xm4 = 0 ;
then m <= 1 by A2, A5, A17, A23, A22, A19, Def28;
hence ( x = 1 & y = len (W .remove (m,n)) ) by ; :: thesis: verum
end;
end;
end;
hence ( x = 1 & y = len (W .remove (m,n)) ) ; :: thesis: verum
end;
end;
end;
hence ( x = 1 & y = len (W .remove (m,n)) ) ; :: thesis: verum
end;
hence W .remove (m,n) is Path-like ; :: thesis: verum
end;
suppose ( not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n ) ; :: thesis: W .remove (m,n) is Path-like
hence W .remove (m,n) is Path-like by Def12; :: thesis: verum
end;
end;
end;
hence W .remove (m,n) is Path-like ; :: thesis: verum