let n, m, i1, j1, i2, j2 be Element of NAT ; :: thesis: ( i1 <= n & j1 <= m & i2 <= n & j2 <= m implies ex fs1, fs2 being FinSequence of NAT st
( ( for i, k1, k2 being Element of NAT st i in dom fs1 & k1 = fs1 . i & k2 = fs2 . i holds
( k1 <= n & k2 <= m ) ) & fs1 . 1 = i1 & fs1 . (len fs1) = i2 & fs2 . 1 = j1 & fs2 . (len fs2) = j2 & len fs1 = len fs2 & len fs1 = ((((i1 -' i2) + (i2 -' i1)) + (j1 -' j2)) + (j2 -' j1)) + 1 & ( for i being Element of NAT st 1 <= i & i < len fs1 holds
fs1 /. i,fs2 /. i,fs1 /. (i + 1),fs2 /. (i + 1) are_adjacent ) ) )

assume that
A1: i1 <= n and
A2: j1 <= m and
A3: i2 <= n and
A4: j2 <= m ; :: thesis: ex fs1, fs2 being FinSequence of NAT st
( ( for i, k1, k2 being Element of NAT st i in dom fs1 & k1 = fs1 . i & k2 = fs2 . i holds
( k1 <= n & k2 <= m ) ) & fs1 . 1 = i1 & fs1 . (len fs1) = i2 & fs2 . 1 = j1 & fs2 . (len fs2) = j2 & len fs1 = len fs2 & len fs1 = ((((i1 -' i2) + (i2 -' i1)) + (j1 -' j2)) + (j2 -' j1)) + 1 & ( for i being Element of NAT st 1 <= i & i < len fs1 holds
fs1 /. i,fs2 /. i,fs1 /. (i + 1),fs2 /. (i + 1) are_adjacent ) )

consider gs1 being FinSequence of NAT such that
A5: gs1 . 1 = i1 and
A6: gs1 . (len gs1) = i2 and
A7: len gs1 = ((i1 -' i2) + (i2 -' i1)) + 1 and
A8: for k, k1 being Element of NAT st 1 <= k & k <= len gs1 & k1 = gs1 . k holds
k1 <= n and
A9: for k being Element of NAT st 1 <= k & k < len gs1 holds
gs1 /. k,gs1 /. (k + 1) are_adjacent by A1, A3, Th6;
consider gs2 being FinSequence of NAT such that
A10: gs2 . 1 = j1 and
A11: gs2 . (len gs2) = j2 and
A12: len gs2 = ((j1 -' j2) + (j2 -' j1)) + 1 and
A13: for k, k1 being Element of NAT st 1 <= k & k <= len gs2 & k1 = gs2 . k holds
k1 <= m and
A14: for k being Element of NAT st 1 <= k & k < len gs2 holds
gs2 /. k,gs2 /. (k + 1) are_adjacent by A2, A4, Th6;
A15: 1 <= len gs2 by ;
then A16: (len gs2) - 1 >= 1 - 1 by XREAL_1:9;
set hs1 = gs1 ^ (((len gs2) -' 1) |-> i2);
set hs2 = (((len gs1) -' 1) |-> j1) ^ gs2;
A17: len (gs1 ^ (((len gs2) -' 1) |-> i2)) = (len gs1) + (len (((len gs2) -' 1) |-> i2)) by FINSEQ_1:22
.= (len gs1) + ((len gs2) -' 1) by CARD_1:def 7
.= (len gs1) + ((len gs2) - 1) by
.= ((len gs1) - 1) + (len gs2) ;
A18: 1 <= len gs1 by ;
then A19: (len gs1) - 1 >= 1 - 1 by XREAL_1:9;
then A20: ((len gs1) - 1) + (len gs2) = ((len gs1) -' 1) + (len gs2) by XREAL_0:def 2
.= (len (((len gs1) -' 1) |-> j1)) + (len gs2) by CARD_1:def 7
.= len ((((len gs1) -' 1) |-> j1) ^ gs2) by FINSEQ_1:22 ;
A21: for i, k1, k2 being Element of NAT st i in dom (gs1 ^ (((len gs2) -' 1) |-> i2)) & k1 = (gs1 ^ (((len gs2) -' 1) |-> i2)) . i & k2 = ((((len gs1) -' 1) |-> j1) ^ gs2) . i holds
( k1 <= n & k2 <= m )
proof
dom ((((len gs1) -' 1) |-> j1) ^ gs2) = Seg ((len (((len gs1) -' 1) |-> j1)) + (len gs2)) by FINSEQ_1:def 7;
then len ((((len gs1) -' 1) |-> j1) ^ gs2) = (len (((len gs1) -' 1) |-> j1)) + (len gs2) by FINSEQ_1:def 3;
then A22: len ((((len gs1) -' 1) |-> j1) ^ gs2) = ((len gs1) -' 1) + (len gs2) by CARD_1:def 7;
let i, k1, k2 be Element of NAT ; :: thesis: ( i in dom (gs1 ^ (((len gs2) -' 1) |-> i2)) & k1 = (gs1 ^ (((len gs2) -' 1) |-> i2)) . i & k2 = ((((len gs1) -' 1) |-> j1) ^ gs2) . i implies ( k1 <= n & k2 <= m ) )
assume that
A23: i in dom (gs1 ^ (((len gs2) -' 1) |-> i2)) and
A24: k1 = (gs1 ^ (((len gs2) -' 1) |-> i2)) . i and
A25: k2 = ((((len gs1) -' 1) |-> j1) ^ gs2) . i ; :: thesis: ( k1 <= n & k2 <= m )
i in Seg (len (gs1 ^ (((len gs2) -' 1) |-> i2))) by ;
then ( ( 1 <= i & i <= (len gs1) -' 1 ) or ( ((len gs1) -' 1) + 1 <= i & i <= len ((((len gs1) -' 1) |-> j1) ^ gs2) ) ) by ;
then ( ( 1 <= i & i <= (len gs1) -' 1 ) or ( ((len gs1) - 1) + 1 <= i & i <= len ((((len gs1) -' 1) |-> j1) ^ gs2) ) ) by ;
then ( ( 1 <= i & i <= (len gs1) - 1 ) or ( (len gs1) - ((len gs1) - 1) <= i - ((len gs1) - 1) & i <= len ((((len gs1) -' 1) |-> j1) ^ gs2) ) ) by ;
then ( ( 1 <= i & i <= (len gs1) - 1 ) or ( 1 <= i - ((len gs1) - 1) & i - ((len gs1) - 1) <= (len ((((len gs1) -' 1) |-> j1) ^ gs2)) - ((len gs1) - 1) ) ) by XREAL_1:9;
then A26: ( ( 1 <= i & i <= (len gs1) - 1 ) or ( 1 <= (i - (len gs1)) + 1 & (i - (len gs1)) + 1 <= ((len ((((len gs1) -' 1) |-> j1) ^ gs2)) - (len gs1)) + 1 ) ) ;
A27: now :: thesis: ( ( 1 <= (i - (len gs1)) + 1 & i - (len gs1) <= (len ((((len gs1) -' 1) |-> j1) ^ gs2)) - (len gs1) & k2 <= m ) or ( 1 <= i & i <= (len gs1) - 1 & k2 <= m ) )
per cases ( ( 1 <= (i - (len gs1)) + 1 & i - (len gs1) <= (len ((((len gs1) -' 1) |-> j1) ^ gs2)) - (len gs1) ) or ( 1 <= i & i <= (len gs1) - 1 ) ) by ;
case A28: ( 1 <= (i - (len gs1)) + 1 & i - (len gs1) <= (len ((((len gs1) -' 1) |-> j1) ^ gs2)) - (len gs1) ) ; :: thesis: k2 <= m
then A29: (i + 1) - (len gs1) <= ((len ((((len gs1) -' 1) |-> j1) ^ gs2)) - (len gs1)) + 1 by XREAL_1:6;
A30: len (((len gs1) -' 1) |-> j1) = (len gs1) -' 1 by CARD_1:def 7;
A31: ((len ((((len gs1) -' 1) |-> j1) ^ gs2)) + 1) - (len gs1) = ((((len gs1) - 1) + (len gs2)) + 1) - (len gs1) by
.= len gs2 ;
A32: (i + 1) - (len gs1) = (i + 1) -' (len gs1) by ;
(i - (len gs1)) + 1 <= ((len ((((len gs1) -' 1) |-> j1) ^ gs2)) - (len gs1)) + 1 by ;
then (i + 1) -' (len gs1) in Seg (len gs2) by ;
then A33: (i + 1) -' (len gs1) in dom gs2 by FINSEQ_1:def 3;
i = ((len gs1) - 1) + ((i + 1) - (len gs1))
.= (len (((len gs1) -' 1) |-> j1)) + ((i + 1) -' (len gs1)) by ;
then ((((len gs1) -' 1) |-> j1) ^ gs2) . i = gs2 . ((i + 1) -' (len gs1)) by ;
hence k2 <= m by A13, A25, A28, A29, A31, A32; :: thesis: verum
end;
case A34: ( 1 <= i & i <= (len gs1) - 1 ) ; :: thesis: k2 <= m
then A35: i <= (len gs1) -' 1 by XREAL_0:def 2;
then i in Seg ((len gs1) -' 1) by ;
then i in Seg (len (((len gs1) -' 1) |-> j1)) by CARD_1:def 7;
then i in dom (((len gs1) -' 1) |-> j1) by FINSEQ_1:def 3;
then ((((len gs1) -' 1) |-> j1) ^ gs2) . i = (((len gs1) -' 1) |-> j1) . i by FINSEQ_1:def 7
.= j1 by ;
hence k2 <= m by ; :: thesis: verum
end;
end;
end;
dom (gs1 ^ (((len gs2) -' 1) |-> i2)) = Seg ((len gs1) + (len (((len gs2) -' 1) |-> i2))) by FINSEQ_1:def 7;
then A36: len (gs1 ^ (((len gs2) -' 1) |-> i2)) = (len gs1) + (len (((len gs2) -' 1) |-> i2)) by FINSEQ_1:def 3;
then A37: (len (gs1 ^ (((len gs2) -' 1) |-> i2))) -' (len gs1) = (len (gs1 ^ (((len gs2) -' 1) |-> i2))) - (len gs1) by XREAL_0:def 2;
A38: len (gs1 ^ (((len gs2) -' 1) |-> i2)) = (len gs1) + ((len gs2) -' 1) by ;
A39: ( ( 1 <= i & i <= len gs1 ) or ( (len gs1) - (len gs1) < i - (len gs1) & i <= len (gs1 ^ (((len gs2) -' 1) |-> i2)) ) ) by ;
now :: thesis: ( ( 1 <= i & i <= len gs1 & k1 <= n ) or ( 0 < i - (len gs1) & i - (len gs1) <= (len (gs1 ^ (((len gs2) -' 1) |-> i2))) -' (len gs1) & k1 <= n ) )
per cases ( ( 1 <= i & i <= len gs1 ) or ( 0 < i - (len gs1) & i - (len gs1) <= (len (gs1 ^ (((len gs2) -' 1) |-> i2))) -' (len gs1) ) ) by ;
case A40: ( 1 <= i & i <= len gs1 ) ; :: thesis: k1 <= n
then i in dom gs1 by FINSEQ_3:25;
then (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = gs1 . i by FINSEQ_1:def 7;
hence k1 <= n by A8, A24, A40; :: thesis: verum
end;
case A41: ( 0 < i - (len gs1) & i - (len gs1) <= (len (gs1 ^ (((len gs2) -' 1) |-> i2))) -' (len gs1) ) ; :: thesis: k1 <= n
then A42: i - (len gs1) = i -' (len gs1) by XREAL_0:def 2;
then A43: 0 + 1 <= i -' (len gs1) by ;
then i -' (len gs1) in Seg ((len (gs1 ^ (((len gs2) -' 1) |-> i2))) -' (len gs1)) by ;
then A44: i -' (len gs1) in Seg ((len gs2) -' 1) by ;
then A45: i -' (len gs1) <= (len gs2) -' 1 by FINSEQ_1:1;
A46: i = (len gs1) + (i - (len gs1)) ;
i -' (len gs1) in Seg (len (((len gs2) -' 1) |-> i2)) by ;
then A47: i -' (len gs1) in dom (((len gs2) -' 1) |-> i2) by FINSEQ_1:def 3;
i -' (len gs1) = i - (len gs1) by ;
then (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = (((len gs2) -' 1) |-> i2) . (i -' (len gs1)) by
.= i2 by ;
hence k1 <= n by ; :: thesis: verum
end;
end;
end;
hence ( k1 <= n & k2 <= m ) by A27; :: thesis: verum
end;
A48: for i being Element of NAT st 1 <= i & i < len (gs1 ^ (((len gs2) -' 1) |-> i2)) holds
(gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1),((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len (gs1 ^ (((len gs2) -' 1) |-> i2)) implies (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1),((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent )
assume that
A49: 1 <= i and
A50: i < len (gs1 ^ (((len gs2) -' 1) |-> i2)) ; :: thesis: (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1),((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent
now :: thesis: ( ( i < len gs1 & ( ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i = ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) ) or ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = (gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent ) ) ) or ( i >= len gs1 & ( ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i = ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) ) or ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = (gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent ) ) ) )
per cases ( i < len gs1 or i >= len gs1 ) ;
case A51: i < len gs1 ; :: thesis: ( ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i = ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) ) or ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = (gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent ) )
then A52: i + 1 <= len gs1 by NAT_1:13;
A53: now :: thesis: ( ( i + 1 <= (len gs1) -' 1 & (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent ) or ( i + 1 > (len gs1) -' 1 & (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent ) )
per cases ( i + 1 <= (len gs1) -' 1 or i + 1 > (len gs1) -' 1 ) ;
case i + 1 <= (len gs1) -' 1 ; :: thesis: (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent
then i + 1 <= (len gs1) - 1 by XREAL_0:def 2;
then (i + 1) + 1 <= ((len gs1) - 1) + 1 by XREAL_1:6;
then A54: i + 1 < len gs1 by NAT_1:13;
then A55: i < len gs1 by NAT_1:13;
then A56: i in dom gs1 by ;
1 < i + 1 by ;
then A57: i + 1 in dom gs1 by ;
A58: dom gs1 c= dom (gs1 ^ (((len gs2) -' 1) |-> i2)) by FINSEQ_1:26;
then A59: (gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) = (gs1 ^ (((len gs2) -' 1) |-> i2)) . (i + 1) by
.= gs1 . (i + 1) by
.= gs1 /. (i + 1) by ;
(gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = (gs1 ^ (((len gs2) -' 1) |-> i2)) . i by
.= gs1 . i by
.= gs1 /. i by ;
hence (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent by A9, A49, A55, A59; :: thesis: verum
end;
case i + 1 > (len gs1) -' 1 ; :: thesis: (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent
0 + 1 <= i + 1 by NAT_1:13;
then A60: i + 1 in dom gs1 by ;
A61: dom gs1 c= dom (gs1 ^ (((len gs2) -' 1) |-> i2)) by FINSEQ_1:26;
then A62: (gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) = (gs1 ^ (((len gs2) -' 1) |-> i2)) . (i + 1) by
.= gs1 . (i + 1) by
.= gs1 /. (i + 1) by ;
A63: i in dom gs1 by ;
then (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = (gs1 ^ (((len gs2) -' 1) |-> i2)) . i by
.= gs1 . i by
.= gs1 /. i by ;
hence (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent by A9, A49, A51, A62; :: thesis: verum
end;
end;
end;
A64: 1 <= i + 1 by ;
A65: now :: thesis: ( ( i + 1 <= (len gs1) -' 1 & ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = j1 ) or ( i + 1 > (len gs1) -' 1 & ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = j1 ) )
per cases ( i + 1 <= (len gs1) -' 1 or i + 1 > (len gs1) -' 1 ) ;
case A66: i + 1 <= (len gs1) -' 1 ; :: thesis: ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = j1
A67: len (((len gs1) -' 1) |-> j1) = (len gs1) -' 1 by CARD_1:def 7;
A68: dom (((len gs1) -' 1) |-> j1) c= dom ((((len gs1) -' 1) |-> j1) ^ gs2) by FINSEQ_1:26;
i + 1 in Seg ((len gs1) -' 1) by ;
then A69: i + 1 in dom (((len gs1) -' 1) |-> j1) by ;
then ((((len gs1) -' 1) |-> j1) ^ gs2) . (i + 1) = (((len gs1) -' 1) |-> j1) . (i + 1) by FINSEQ_1:def 7
.= j1 by ;
hence ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = j1 by ; :: thesis: verum
end;
case A70: i + 1 > (len gs1) -' 1 ; :: thesis: ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = j1
A71: ((len gs1) -' 1) + 1 = ((len gs1) - 1) + 1 by
.= len gs1 ;
((len gs1) -' 1) + 1 <= i + 1 by ;
then A72: len gs1 = i + 1 by ;
dom ((((len gs1) -' 1) |-> j1) ^ gs2) = Seg ((len (((len gs1) -' 1) |-> j1)) + (len gs2)) by FINSEQ_1:def 7;
then len ((((len gs1) -' 1) |-> j1) ^ gs2) = (len (((len gs1) -' 1) |-> j1)) + (len gs2) by FINSEQ_1:def 3
.= ((len gs1) -' 1) + (len gs2) by CARD_1:def 7
.= ((len gs1) - 1) + (len gs2) by
.= (len gs1) + ((len gs2) - 1)
.= (len gs1) + ((len gs2) -' 1) by ;
then len gs1 <= len ((((len gs1) -' 1) |-> j1) ^ gs2) by NAT_1:11;
then len gs1 in Seg (len ((((len gs1) -' 1) |-> j1) ^ gs2)) by ;
then A73: i + 1 in dom ((((len gs1) -' 1) |-> j1) ^ gs2) by ;
1 in Seg (len gs2) by ;
then A74: 1 in dom gs2 by FINSEQ_1:def 3;
(len (((len gs1) -' 1) |-> j1)) + 1 = i + 1 by ;
then ((((len gs1) -' 1) |-> j1) ^ gs2) . (i + 1) = j1 by ;
hence ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = j1 by ; :: thesis: verum
end;
end;
end;
A75: len (((len gs1) -' 1) |-> j1) = (len gs1) -' 1 by CARD_1:def 7;
A76: dom (((len gs1) -' 1) |-> j1) c= dom ((((len gs1) -' 1) |-> j1) ^ gs2) by FINSEQ_1:26;
(i + 1) - 1 <= (len gs1) - 1 by ;
then A77: i <= (len gs1) -' 1 by XREAL_0:def 2;
then i in Seg ((len gs1) -' 1) by ;
then A78: i in dom (((len gs1) -' 1) |-> j1) by ;
then ((((len gs1) -' 1) |-> j1) ^ gs2) . i = (((len gs1) -' 1) |-> j1) . i by FINSEQ_1:def 7
.= j1 by ;
hence ( ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i = ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) ) or ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = (gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent ) ) by ; :: thesis: verum
end;
case A79: i >= len gs1 ; :: thesis: ( ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i = ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) ) or ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = (gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent ) )
then A80: 0 <= (i + 1) - (len gs1) by ;
A81: (len (((len gs1) -' 1) |-> j1)) + (((i + 1) -' (len gs1)) + 1) = ((len gs1) -' 1) + (((i + 1) -' (len gs1)) + 1) by CARD_1:def 7
.= ((len gs1) - 1) + (((i + 1) -' (len gs1)) + 1) by
.= ((len gs1) - 1) + (((i + 1) - (len gs1)) + 1) by
.= i + 1 ;
A82: i + 1 = (len gs1) + ((i + 1) - (len gs1))
.= (len gs1) + ((i + 1) -' (len gs1)) by ;
A83: i - (len gs1) >= 0 by ;
then 0 + 1 <= (i - (len gs1)) + 1 by XREAL_1:6;
then A84: 1 <= (i + 1) -' (len gs1) by ;
A85: i - (len gs1) = i -' (len gs1) by ;
A86: now :: thesis: ( not 1 <= i -' (len gs1) implies (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = i2 )
assume not 1 <= i -' (len gs1) ; :: thesis: (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = i2
then i -' (len gs1) < 0 + 1 ;
then A87: i -' (len gs1) = 0 by NAT_1:13;
len gs1 in Seg (len gs1) by ;
then i in dom gs1 by ;
hence (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = i2 by ; :: thesis: verum
end;
A88: ((i + 1) - (len gs1)) + (len gs1) <= ((len gs2) - 1) + (len gs1) by ;
then (i + 1) - (len gs1) <= (len gs2) - 1 by XREAL_1:6;
then (i + 1) - (len gs1) <= (len gs2) -' 1 by XREAL_0:def 2;
then A89: (i + 1) -' (len gs1) <= (len gs2) -' 1 by XREAL_0:def 2;
(i - (len gs1)) + 1 >= 0 + 1 by ;
then A90: 1 <= (i + 1) -' (len gs1) by ;
len (((len gs2) -' 1) |-> i2) = (len gs2) -' 1 by CARD_1:def 7;
then (i + 1) -' (len gs1) in Seg (len (((len gs2) -' 1) |-> i2)) by ;
then (i + 1) -' (len gs1) in dom (((len gs2) -' 1) |-> i2) by FINSEQ_1:def 3;
then A91: (gs1 ^ (((len gs2) -' 1) |-> i2)) . (i + 1) = (((len gs2) -' 1) |-> i2) . ((i + 1) -' (len gs1)) by
.= i2 by ;
A92: (len (((len gs1) -' 1) |-> j1)) + ((i + 1) -' (len gs1)) = ((len gs1) -' 1) + ((i + 1) -' (len gs1)) by CARD_1:def 7
.= ((len gs1) - 1) + ((i + 1) -' (len gs1)) by
.= ((len gs1) - 1) + ((i - (len gs1)) + 1) by
.= i ;
len (gs1 ^ (((len gs2) -' 1) |-> i2)) = (len gs1) + (len (((len gs2) -' 1) |-> i2)) by FINSEQ_1:22
.= (len gs1) + ((len gs2) -' 1) by CARD_1:def 7 ;
then i - (len gs1) < ((len gs1) + ((len gs2) -' 1)) - (len gs1) by ;
then A93: i -' (len gs1) <= (len gs2) -' 1 by XREAL_0:def 2;
i - ((len gs1) - 1) < (((len gs1) - 1) + (len gs2)) - ((len gs1) - 1) by ;
then A94: (i + 1) -' (len gs1) < len gs2 by ;
then ( 1 <= ((i + 1) -' (len gs1)) + 1 & len gs2 >= ((i + 1) -' (len gs1)) + 1 ) by ;
then ((i + 1) -' (len gs1)) + 1 in Seg (len gs2) by FINSEQ_1:1;
then A95: ((i + 1) -' (len gs1)) + 1 in dom gs2 by FINSEQ_1:def 3;
(len gs2) -' 1 <= ((len gs2) -' 1) + 1 by NAT_1:11;
then (i + 1) -' (len gs1) <= ((len gs2) -' 1) + 1 by ;
then (i + 1) -' (len gs1) <= ((len gs2) - 1) + 1 by ;
then A96: (i + 1) -' (len gs1) in dom gs2 by ;
A97: len (((len gs2) -' 1) |-> i2) = (len gs2) -' 1 by CARD_1:def 7;
A98: now :: thesis: ( 1 <= i -' (len gs1) implies (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = i2 )
A99: i = (len gs1) + (i - (len gs1))
.= (len gs1) + (i -' (len gs1)) by ;
assume A100: 1 <= i -' (len gs1) ; :: thesis: (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = i2
then i -' (len gs1) in Seg (len (((len gs2) -' 1) |-> i2)) by ;
then i -' (len gs1) in dom (((len gs2) -' 1) |-> i2) by FINSEQ_1:def 3;
then (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = (((len gs2) -' 1) |-> i2) . (i -' (len gs1)) by
.= i2 by ;
hence (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = i2 ; :: thesis: verum
end;
i in dom ((((len gs1) -' 1) |-> j1) ^ gs2) by ;
then A101: ((((len gs1) -' 1) |-> j1) ^ gs2) /. i = ((((len gs1) -' 1) |-> j1) ^ gs2) . ((len (((len gs1) -' 1) |-> j1)) + ((i + 1) -' (len gs1))) by
.= gs2 . ((i + 1) -' (len gs1)) by
.= gs2 /. ((i + 1) -' (len gs1)) by ;
i in dom (gs1 ^ (((len gs2) -' 1) |-> i2)) by ;
then A102: (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = i2 by ;
( i + 1 <= len (gs1 ^ (((len gs2) -' 1) |-> i2)) & 0 + 1 <= i + 1 ) by ;
then A103: i + 1 in Seg (len (gs1 ^ (((len gs2) -' 1) |-> i2))) by FINSEQ_1:1;
then i + 1 in dom ((((len gs1) -' 1) |-> j1) ^ gs2) by ;
then A104: ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = ((((len gs1) -' 1) |-> j1) ^ gs2) . ((len (((len gs1) -' 1) |-> j1)) + (((i + 1) -' (len gs1)) + 1)) by
.= gs2 . (((i + 1) -' (len gs1)) + 1) by
.= gs2 /. (((i + 1) -' (len gs1)) + 1) by ;
i + 1 in dom (gs1 ^ (((len gs2) -' 1) |-> i2)) by ;
hence ( ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i = ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) ) or ( (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = (gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) & ((((len gs1) -' 1) |-> j1) ^ gs2) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent ) ) by ; :: thesis: verum
end;
end;
end;
hence (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,((((len gs1) -' 1) |-> j1) ^ gs2) /. i,(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1),((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) are_adjacent ; :: thesis: verum
end;
A105: now :: thesis: ( ( (len gs1) -' 1 = 0 & ((((len gs1) -' 1) |-> j1) ^ gs2) . 1 = j1 & ((((len gs1) -' 1) |-> j1) ^ gs2) . (len ((((len gs1) -' 1) |-> j1) ^ gs2)) = j2 ) or ( (len gs1) -' 1 <> 0 & ((((len gs1) -' 1) |-> j1) ^ gs2) . 1 = j1 & ((((len gs1) -' 1) |-> j1) ^ gs2) . (len ((((len gs1) -' 1) |-> j1) ^ gs2)) = j2 ) )
per cases ( (len gs1) -' 1 = 0 or (len gs1) -' 1 <> 0 ) ;
case (len gs1) -' 1 = 0 ; :: thesis: ( ((((len gs1) -' 1) |-> j1) ^ gs2) . 1 = j1 & ((((len gs1) -' 1) |-> j1) ^ gs2) . (len ((((len gs1) -' 1) |-> j1) ^ gs2)) = j2 )
then (((len gs1) -' 1) |-> j1) ^ gs2 = () ^ gs2
.= gs2 by FINSEQ_1:34 ;
hence ( ((((len gs1) -' 1) |-> j1) ^ gs2) . 1 = j1 & ((((len gs1) -' 1) |-> j1) ^ gs2) . (len ((((len gs1) -' 1) |-> j1) ^ gs2)) = j2 ) by ; :: thesis: verum
end;
case A106: (len gs1) -' 1 <> 0 ; :: thesis: ( ((((len gs1) -' 1) |-> j1) ^ gs2) . 1 = j1 & ((((len gs1) -' 1) |-> j1) ^ gs2) . (len ((((len gs1) -' 1) |-> j1) ^ gs2)) = j2 )
len (((len gs1) -' 1) |-> j1) = (len gs1) -' 1 by CARD_1:def 7;
then A107: 0 + 1 <= len (((len gs1) -' 1) |-> j1) by ;
then 1 in dom (((len gs1) -' 1) |-> j1) by FINSEQ_3:25;
then A108: ((((len gs1) -' 1) |-> j1) ^ gs2) . 1 = (((len gs1) -' 1) |-> j1) . 1 by FINSEQ_1:def 7;
1 <= len gs2 by ;
then A109: len gs2 in dom gs2 by FINSEQ_3:25;
( len (((len gs1) -' 1) |-> j1) = (len gs1) -' 1 & len ((((len gs1) -' 1) |-> j1) ^ gs2) = (len (((len gs1) -' 1) |-> j1)) + (len gs2) ) by ;
hence ( ((((len gs1) -' 1) |-> j1) ^ gs2) . 1 = j1 & ((((len gs1) -' 1) |-> j1) ^ gs2) . (len ((((len gs1) -' 1) |-> j1) ^ gs2)) = j2 ) by ; :: thesis: verum
end;
end;
end;
A110: 1 in dom gs1 by ;
now :: thesis: ( ( (len gs2) -' 1 = 0 & (gs1 ^ (((len gs2) -' 1) |-> i2)) . 1 = i1 & (gs1 ^ (((len gs2) -' 1) |-> i2)) . (len (gs1 ^ (((len gs2) -' 1) |-> i2))) = i2 ) or ( (len gs2) -' 1 <> 0 & (gs1 ^ (((len gs2) -' 1) |-> i2)) . 1 = i1 & (gs1 ^ (((len gs2) -' 1) |-> i2)) . (len (gs1 ^ (((len gs2) -' 1) |-> i2))) = i2 ) )
per cases ( (len gs2) -' 1 = 0 or (len gs2) -' 1 <> 0 ) ;
case (len gs2) -' 1 = 0 ; :: thesis: ( (gs1 ^ (((len gs2) -' 1) |-> i2)) . 1 = i1 & (gs1 ^ (((len gs2) -' 1) |-> i2)) . (len (gs1 ^ (((len gs2) -' 1) |-> i2))) = i2 )
then gs1 ^ (((len gs2) -' 1) |-> i2) = gs1 ^ ()
.= gs1 by FINSEQ_1:34 ;
hence ( (gs1 ^ (((len gs2) -' 1) |-> i2)) . 1 = i1 & (gs1 ^ (((len gs2) -' 1) |-> i2)) . (len (gs1 ^ (((len gs2) -' 1) |-> i2))) = i2 ) by A5, A6; :: thesis: verum
end;
case (len gs2) -' 1 <> 0 ; :: thesis: ( (gs1 ^ (((len gs2) -' 1) |-> i2)) . 1 = i1 & (gs1 ^ (((len gs2) -' 1) |-> i2)) . (len (gs1 ^ (((len gs2) -' 1) |-> i2))) = i2 )
then A111: 0 + 1 <= (len gs2) -' 1 by NAT_1:13;
A112: len (gs1 ^ (((len gs2) -' 1) |-> i2)) = (len gs1) + (len (((len gs2) -' 1) |-> i2)) by FINSEQ_1:22;
len (((len gs2) -' 1) |-> i2) = (len gs2) -' 1 by CARD_1:def 7;
then ( len (((len gs2) -' 1) |-> i2) in dom (((len gs2) -' 1) |-> i2) & (((len gs2) -' 1) |-> i2) . (len (((len gs2) -' 1) |-> i2)) = i2 ) by ;
hence ( (gs1 ^ (((len gs2) -' 1) |-> i2)) . 1 = i1 & (gs1 ^ (((len gs2) -' 1) |-> i2)) . (len (gs1 ^ (((len gs2) -' 1) |-> i2))) = i2 ) by ; :: thesis: verum
end;
end;
end;
hence ex fs1, fs2 being FinSequence of NAT st
( ( for i, k1, k2 being Element of NAT st i in dom fs1 & k1 = fs1 . i & k2 = fs2 . i holds
( k1 <= n & k2 <= m ) ) & fs1 . 1 = i1 & fs1 . (len fs1) = i2 & fs2 . 1 = j1 & fs2 . (len fs2) = j2 & len fs1 = len fs2 & len fs1 = ((((i1 -' i2) + (i2 -' i1)) + (j1 -' j2)) + (j2 -' j1)) + 1 & ( for i being Element of NAT st 1 <= i & i < len fs1 holds
fs1 /. i,fs2 /. i,fs1 /. (i + 1),fs2 /. (i + 1) are_adjacent ) ) by A7, A12, A17, A20, A105, A21, A48; :: thesis: verum