let n, m, i1, j1, i2, j2 be Element of NAT ; ( 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
; 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 A12, NAT_1:11;
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 A16, XREAL_0:def 2
.=
((len gs1) - 1) + (len gs2)
;
A18:
1 <= len gs1
by A7, NAT_1:11;
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 ;
( 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
;
( k1 <= n & k2 <= m )
i in Seg (len (gs1 ^ (((len gs2) -' 1) |-> i2)))
by A23, FINSEQ_1:def 3;
then
( ( 1
<= i &
i <= (len gs1) -' 1 ) or (
((len gs1) -' 1) + 1
<= i &
i <= len ((((len gs1) -' 1) |-> j1) ^ gs2) ) )
by A17, A20, FINSEQ_1:1, NAT_1:13;
then
( ( 1
<= i &
i <= (len gs1) -' 1 ) or (
((len gs1) - 1) + 1
<= i &
i <= len ((((len gs1) -' 1) |-> j1) ^ gs2) ) )
by A19, XREAL_0:def 2;
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 XREAL_0:def 2, XREAL_1:9;
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 ( ( 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 A26, XREAL_1:6;
case A28:
( 1
<= (i - (len gs1)) + 1 &
i - (len gs1) <= (len ((((len gs1) -' 1) |-> j1) ^ gs2)) - (len gs1) )
;
k2 <= mthen 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 A19, A22, XREAL_0:def 2
.=
len gs2
;
A32:
(i + 1) - (len gs1) = (i + 1) -' (len gs1)
by A28, XREAL_0:def 2;
(i - (len gs1)) + 1
<= ((len ((((len gs1) -' 1) |-> j1) ^ gs2)) - (len gs1)) + 1
by A28, XREAL_1:6;
then
(i + 1) -' (len gs1) in Seg (len gs2)
by A28, A31, A32, FINSEQ_1:1;
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 A19, A32, A30, XREAL_0:def 2
;
then
((((len gs1) -' 1) |-> j1) ^ gs2) . i = gs2 . ((i + 1) -' (len gs1))
by A33, FINSEQ_1:def 7;
hence
k2 <= m
by A13, A25, A28, A29, A31, A32;
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 A36, CARD_1:def 7;
A39:
( ( 1
<= i &
i <= len gs1 ) or (
(len gs1) - (len gs1) < i - (len gs1) &
i <= len (gs1 ^ (((len gs2) -' 1) |-> i2)) ) )
by A23, FINSEQ_3:25, XREAL_1:9;
now ( ( 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 A37, A39, XREAL_1:9;
case A41:
(
0 < i - (len gs1) &
i - (len gs1) <= (len (gs1 ^ (((len gs2) -' 1) |-> i2))) -' (len gs1) )
;
k1 <= nthen A42:
i - (len gs1) = i -' (len gs1)
by XREAL_0:def 2;
then A43:
0 + 1
<= i -' (len gs1)
by A41, NAT_1:13;
then
i -' (len gs1) in Seg ((len (gs1 ^ (((len gs2) -' 1) |-> i2))) -' (len gs1))
by A41, A42, FINSEQ_1:1;
then A44:
i -' (len gs1) in Seg ((len gs2) -' 1)
by A38, NAT_D:34;
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 A44, CARD_1:def 7;
then A47:
i -' (len gs1) in dom (((len gs2) -' 1) |-> i2)
by FINSEQ_1:def 3;
i -' (len gs1) = i - (len gs1)
by A41, XREAL_0:def 2;
then (gs1 ^ (((len gs2) -' 1) |-> i2)) . i =
(((len gs2) -' 1) |-> i2) . (i -' (len gs1))
by A47, A46, FINSEQ_1:def 7
.=
i2
by A43, A45, Lm1
;
hence
k1 <= n
by A3, A24;
verum end; end; end;
hence
(
k1 <= n &
k2 <= m )
by A27;
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 ;
( 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))
;
(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 ( ( 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
;
( ( (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 ( ( 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
;
(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 A49, FINSEQ_3:25;
1
< i + 1
by A49, NAT_1:13;
then A57:
i + 1
in dom gs1
by A54, FINSEQ_3:25;
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 A57, PARTFUN1:def 6
.=
gs1 . (i + 1)
by A57, FINSEQ_1:def 7
.=
gs1 /. (i + 1)
by A57, PARTFUN1:def 6
;
(gs1 ^ (((len gs2) -' 1) |-> i2)) /. i =
(gs1 ^ (((len gs2) -' 1) |-> i2)) . i
by A58, A56, PARTFUN1:def 6
.=
gs1 . i
by A56, FINSEQ_1:def 7
.=
gs1 /. i
by A56, PARTFUN1:def 6
;
hence
(gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,
(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent
by A9, A49, A55, A59;
verum end; case
i + 1
> (len gs1) -' 1
;
(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 A52, FINSEQ_3:25;
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 A60, PARTFUN1:def 6
.=
gs1 . (i + 1)
by A60, FINSEQ_1:def 7
.=
gs1 /. (i + 1)
by A60, PARTFUN1:def 6
;
A63:
i in dom gs1
by A49, A51, FINSEQ_3:25;
then (gs1 ^ (((len gs2) -' 1) |-> i2)) /. i =
(gs1 ^ (((len gs2) -' 1) |-> i2)) . i
by A61, PARTFUN1:def 6
.=
gs1 . i
by A63, FINSEQ_1:def 7
.=
gs1 /. i
by A63, PARTFUN1:def 6
;
hence
(gs1 ^ (((len gs2) -' 1) |-> i2)) /. i,
(gs1 ^ (((len gs2) -' 1) |-> i2)) /. (i + 1) are_adjacent
by A9, A49, A51, A62;
verum end; end; end; A64:
1
<= i + 1
by A49, NAT_1:13;
A65:
now ( ( 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 A70:
i + 1
> (len gs1) -' 1
;
((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = j1A71:
((len gs1) -' 1) + 1 =
((len gs1) - 1) + 1
by A7, XREAL_0:def 2
.=
len gs1
;
((len gs1) -' 1) + 1
<= i + 1
by A70, NAT_1:13;
then A72:
len gs1 = i + 1
by A52, A71, XXREAL_0:1;
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 A7, XREAL_0:def 2
.=
(len gs1) + ((len gs2) - 1)
.=
(len gs1) + ((len gs2) -' 1)
by A12, XREAL_0:def 2
;
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 A18, FINSEQ_1:1;
then A73:
i + 1
in dom ((((len gs1) -' 1) |-> j1) ^ gs2)
by A72, FINSEQ_1:def 3;
1
in Seg (len gs2)
by A15, FINSEQ_1:1;
then A74:
1
in dom gs2
by FINSEQ_1:def 3;
(len (((len gs1) -' 1) |-> j1)) + 1
= i + 1
by A71, A72, CARD_1:def 7;
then
((((len gs1) -' 1) |-> j1) ^ gs2) . (i + 1) = j1
by A10, A74, FINSEQ_1:def 7;
hence
((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = j1
by A73, PARTFUN1:def 6;
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 A52, XREAL_1:9;
then A77:
i <= (len gs1) -' 1
by XREAL_0:def 2;
then
i in Seg ((len gs1) -' 1)
by A49, FINSEQ_1:1;
then A78:
i in dom (((len gs1) -' 1) |-> j1)
by A75, FINSEQ_1:def 3;
then ((((len gs1) -' 1) |-> j1) ^ gs2) . i =
(((len gs1) -' 1) |-> j1) . i
by FINSEQ_1:def 7
.=
j1
by A49, A77, Lm1
;
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 A78, A76, A65, A53, PARTFUN1:def 6;
verum end; case A79:
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 ) )then A80:
0 <= (i + 1) - (len gs1)
by NAT_1:12, XREAL_1:48;
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 A19, XREAL_0:def 2
.=
((len gs1) - 1) + (((i + 1) - (len gs1)) + 1)
by A80, XREAL_0:def 2
.=
i + 1
;
A82:
i + 1 =
(len gs1) + ((i + 1) - (len gs1))
.=
(len gs1) + ((i + 1) -' (len gs1))
by A80, XREAL_0:def 2
;
A83:
i - (len gs1) >= 0
by A79, XREAL_1:48;
then
0 + 1
<= (i - (len gs1)) + 1
by XREAL_1:6;
then A84:
1
<= (i + 1) -' (len gs1)
by A80, XREAL_0:def 2;
A85:
i - (len gs1) = i -' (len gs1)
by A83, XREAL_0:def 2;
A88:
((i + 1) - (len gs1)) + (len gs1) <= ((len gs2) - 1) + (len gs1)
by A17, A50, NAT_1:13;
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 A83, XREAL_1:6;
then A90:
1
<= (i + 1) -' (len gs1)
by A88, XREAL_0:def 2;
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 A90, A89, FINSEQ_1:1;
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 A82, FINSEQ_1:def 7
.=
i2
by A90, A89, Lm1
;
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 A19, XREAL_0:def 2
.=
((len gs1) - 1) + ((i - (len gs1)) + 1)
by A80, XREAL_0:def 2
.=
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 A50, XREAL_1:9;
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 A17, A50, XREAL_1:9;
then A94:
(i + 1) -' (len gs1) < len gs2
by A80, XREAL_0:def 2;
then
( 1
<= ((i + 1) -' (len gs1)) + 1 &
len gs2 >= ((i + 1) -' (len gs1)) + 1 )
by NAT_1:11, NAT_1:13;
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 A89, XXREAL_0:2;
then
(i + 1) -' (len gs1) <= ((len gs2) - 1) + 1
by A16, XREAL_0:def 2;
then A96:
(i + 1) -' (len gs1) in dom gs2
by A90, FINSEQ_3:25;
A97:
len (((len gs2) -' 1) |-> i2) = (len gs2) -' 1
by CARD_1:def 7;
i in dom ((((len gs1) -' 1) |-> j1) ^ gs2)
by A17, A20, A49, A50, FINSEQ_3:25;
then A101:
((((len gs1) -' 1) |-> j1) ^ gs2) /. i =
((((len gs1) -' 1) |-> j1) ^ gs2) . ((len (((len gs1) -' 1) |-> j1)) + ((i + 1) -' (len gs1)))
by A92, PARTFUN1:def 6
.=
gs2 . ((i + 1) -' (len gs1))
by A96, FINSEQ_1:def 7
.=
gs2 /. ((i + 1) -' (len gs1))
by A96, PARTFUN1:def 6
;
i in dom (gs1 ^ (((len gs2) -' 1) |-> i2))
by A49, A50, FINSEQ_3:25;
then A102:
(gs1 ^ (((len gs2) -' 1) |-> i2)) /. i = i2
by A86, A98, PARTFUN1:def 6;
(
i + 1
<= len (gs1 ^ (((len gs2) -' 1) |-> i2)) &
0 + 1
<= i + 1 )
by A50, NAT_1:13;
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 A17, A20, FINSEQ_1:def 3;
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 A81, PARTFUN1:def 6
.=
gs2 . (((i + 1) -' (len gs1)) + 1)
by A95, FINSEQ_1:def 7
.=
gs2 /. (((i + 1) -' (len gs1)) + 1)
by A95, PARTFUN1:def 6
;
i + 1
in dom (gs1 ^ (((len gs2) -' 1) |-> i2))
by A103, FINSEQ_1:def 3;
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 A14, A102, A91, A84, A94, A104, A101, PARTFUN1:def 6;
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
;
verum
end;
A110:
1 in dom gs1
by A18, FINSEQ_3:25;
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; verum