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 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 ; :: 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 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 :: 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 A26, XREAL_1:6;

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 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; :: 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 A34, FINSEQ_1:1;
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 A34, A35, Lm1 ;
hence k2 <= m by A2, A25; :: 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 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 :: 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 A37, A39, XREAL_1:9;

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 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; :: 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 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; :: 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 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; :: thesis: verum

end;

end;

end;

A64: 1 <= i + 1 by A49, NAT_1:13;

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 A64, A66, FINSEQ_1:1;
then A69: i + 1 in dom (((len gs1) -' 1) |-> j1) by A67, FINSEQ_1:def 3;
then ((((len gs1) -' 1) |-> j1) ^ gs2) . (i + 1) = (((len gs1) -' 1) |-> j1) . (i + 1) by FINSEQ_1:def 7
.= j1 by A64, A66, Lm1 ;
hence ((((len gs1) -' 1) |-> j1) ^ gs2) /. (i + 1) = j1 by A69, A68, PARTFUN1:def 6; :: 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 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; :: 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 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; :: 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 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;

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 A7, FINSEQ_1:3;
then i in dom gs1 by A85, A87, FINSEQ_1:def 3;
hence (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = i2 by A6, A85, A87, FINSEQ_1:def 7; :: thesis: verum

end;

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;

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 A83, XREAL_0:def 2 ;
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 A93, A97, FINSEQ_1:1;
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 A99, FINSEQ_1:def 7
.= i2 by A93, A100, Lm1 ;
hence (gs1 ^ (((len gs2) -' 1) |-> i2)) . i = i2 ; :: thesis: verum

end;

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; :: 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 = (<*> NAT) ^ 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 A10, A11; :: 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 A106, NAT_1:13;
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 A12, NAT_1:11;
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 CARD_1:def 7, FINSEQ_1:22;
hence ( ((((len gs1) -' 1) |-> j1) ^ gs2) . 1 = j1 & ((((len gs1) -' 1) |-> j1) ^ gs2) . (len ((((len gs1) -' 1) |-> j1) ^ gs2)) = j2 ) by A11, A107, A108, A109, Lm1, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

A110: 1 in dom gs1 by A18, FINSEQ_3:25;

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 ^ (<*> NAT)
.= 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 A111, Lm1, FINSEQ_3:25;
hence ( (gs1 ^ (((len gs2) -' 1) |-> i2)) . 1 = i1 & (gs1 ^ (((len gs2) -' 1) |-> i2)) . (len (gs1 ^ (((len gs2) -' 1) |-> i2))) = i2 ) by A5, A110, A112, FINSEQ_1:def 7; :: 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