let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: for D being set
for M being Matrix of D st ( for n being Element of NAT st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * m,k & f1 /. (n + 1) = M * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for n being Element of NAT st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * m,k & f2 /. (n + 1) = M * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. (len f1) = M * m,k & f2 /. 1 = M * i,j & len f1 in dom f1 & 1 in dom f2 holds
(abs (m - i)) + (abs (k - j)) = 1 ) holds
for n being Element of NAT st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * m,k & (f1 ^ f2) /. (n + 1) = M * i,j holds
(abs (m - i)) + (abs (k - j)) = 1
let D be set ; :: thesis: for M being Matrix of D st ( for n being Element of NAT st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * m,k & f1 /. (n + 1) = M * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for n being Element of NAT st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * m,k & f2 /. (n + 1) = M * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. (len f1) = M * m,k & f2 /. 1 = M * i,j & len f1 in dom f1 & 1 in dom f2 holds
(abs (m - i)) + (abs (k - j)) = 1 ) holds
for n being Element of NAT st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * m,k & (f1 ^ f2) /. (n + 1) = M * i,j holds
(abs (m - i)) + (abs (k - j)) = 1
let M be Matrix of D; :: thesis: ( ( for n being Element of NAT st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * m,k & f1 /. (n + 1) = M * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for n being Element of NAT st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * m,k & f2 /. (n + 1) = M * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 ) & ( for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. (len f1) = M * m,k & f2 /. 1 = M * i,j & len f1 in dom f1 & 1 in dom f2 holds
(abs (m - i)) + (abs (k - j)) = 1 ) implies for n being Element of NAT st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * m,k & (f1 ^ f2) /. (n + 1) = M * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 )
assume that
A1:
for n being Element of NAT st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * m,k & f1 /. (n + 1) = M * i,j holds
(abs (m - i)) + (abs (k - j)) = 1
and
A2:
for n being Element of NAT st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * m,k & f2 /. (n + 1) = M * i,j holds
(abs (m - i)) + (abs (k - j)) = 1
and
A3:
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & f1 /. (len f1) = M * m,k & f2 /. 1 = M * i,j & len f1 in dom f1 & 1 in dom f2 holds
(abs (m - i)) + (abs (k - j)) = 1
; :: thesis: for n being Element of NAT st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * m,k & (f1 ^ f2) /. (n + 1) = M * i,j holds
(abs (m - i)) + (abs (k - j)) = 1
let n be Element of NAT ; :: thesis: ( n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) implies for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * m,k & (f1 ^ f2) /. (n + 1) = M * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 )
assume A4:
( n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) )
; :: thesis: for m, k, i, j being Element of NAT st [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * m,k & (f1 ^ f2) /. (n + 1) = M * i,j holds
(abs (m - i)) + (abs (k - j)) = 1
let m, k, i, j be Element of NAT ; :: thesis: ( [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * m,k & (f1 ^ f2) /. (n + 1) = M * i,j implies (abs (m - i)) + (abs (k - j)) = 1 )
assume A5:
( [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * m,k & (f1 ^ f2) /. (n + 1) = M * i,j )
; :: thesis: (abs (m - i)) + (abs (k - j)) = 1
A6:
( dom (f1 ^ f2) = Seg (len (f1 ^ f2)) & dom f2 = Seg (len f2) & dom f1 = Seg (len f1) )
by FINSEQ_1:def 3;
per cases
( n in dom f1 or ex m being Nat st
( m in dom f2 & n = (len f1) + m ) )
by A4, FINSEQ_1:38;
suppose A7:
n in dom f1
;
:: thesis: (abs (m - i)) + (abs (k - j)) = 1then A8:
(
f1 /. n = M * m,
k & 1
<= n &
n <= len f1 )
by A5, A6, FINSEQ_1:3, FINSEQ_4:83;
now per cases
( n + 1 in dom f1 or ex m being Nat st
( m in dom f2 & n + 1 = (len f1) + m ) )
by A4, FINSEQ_1:38;
suppose
ex
m being
Nat st
(
m in dom f2 &
n + 1
= (len f1) + m )
;
:: thesis: (abs (m - i)) + (abs (k - j)) = 1then consider mm being
Nat such that A10:
(
mm in dom f2 &
n + 1
= (len f1) + mm )
;
1
<= mm
by A10, FINSEQ_3:27;
then A11:
0 <= mm - 1
by XREAL_1:50;
(len f1) + (mm - 1) <= (len f1) + 0
by A6, A7, A10, FINSEQ_1:3;
then A12:
mm - 1
= 0
by A11, XREAL_1:8;
then A13:
M * i,
j = f2 /. 1
by A5, A10, FINSEQ_4:84;
M * m,
k = f1 /. (len f1)
by A5, A7, A10, A12, FINSEQ_4:83;
hence
(abs (m - i)) + (abs (k - j)) = 1
by A3, A5, A7, A10, A12, A13;
:: thesis: verum end; hence
(abs (m - i)) + (abs (k - j)) = 1
;
:: thesis: verum end; suppose
ex
m being
Nat st
(
m in dom f2 &
n = (len f1) + m )
;
:: thesis: (abs (m - i)) + (abs (k - j)) = 1then consider mm being
Nat such that A14:
(
mm in dom f2 &
n = (len f1) + mm )
;
( 1
<= mm &
mm <= mm + 1 &
n + 1
<= len (f1 ^ f2) )
by A4, A14, FINSEQ_3:27, NAT_1:11;
then
(
((len f1) + mm) + 1
<= (len f1) + (len f2) &
((len f1) + mm) + 1
= (len f1) + (mm + 1) )
by A14, FINSEQ_1:35;
then
( 1
<= mm + 1 &
mm + 1
<= len f2 )
by NAT_1:11, XREAL_1:8;
then A15:
mm + 1
in dom f2
by FINSEQ_3:27;
A16:
M * i,
j =
(f1 ^ f2) /. ((len f1) + (mm + 1))
by A5, A14
.=
f2 /. (mm + 1)
by A15, FINSEQ_4:84
;
M * m,
k = f2 /. mm
by A5, A14, FINSEQ_4:84;
hence
(abs (m - i)) + (abs (k - j)) = 1
by A2, A5, A14, A15, A16;
:: thesis: verum end;