let f1, f2 be FinSequence of (TOP-REAL 2); for D being set
for M being Matrix of D st ( for n being Nat st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * (m,k) & f1 /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) & ( for n being Nat st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * (m,k) & f2 /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) & ( for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1 ) holds
for n being Nat st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1
let D be set ; for M being Matrix of D st ( for n being Nat st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * (m,k) & f1 /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) & ( for n being Nat st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * (m,k) & f2 /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) & ( for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1 ) holds
for n being Nat st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1
let M be Matrix of D; ( ( for n being Nat st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * (m,k) & f1 /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) & ( for n being Nat st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * (m,k) & f2 /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ) & ( for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1 ) implies for n being Nat st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1 )
assume that
A1:
for n being Nat st n in dom f1 & n + 1 in dom f1 holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f1 /. n = M * (m,k) & f1 /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1
and
A2:
for n being Nat st n in dom f2 & n + 1 in dom f2 holds
for m, k, i, j being Nat st [m,k] in Indices M & [i,j] in Indices M & f2 /. n = M * (m,k) & f2 /. (n + 1) = M * (i,j) holds
|.(m - i).| + |.(k - j).| = 1
and
A3:
for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1
; for n being Nat st n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) holds
for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1
let n be Nat; ( n in dom (f1 ^ f2) & n + 1 in dom (f1 ^ f2) implies for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1 )
assume that
A4:
n in dom (f1 ^ f2)
and
A5:
n + 1 in dom (f1 ^ f2)
; for m, k, i, j being 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
|.(m - i).| + |.(k - j).| = 1
let m, k, i, j be Nat; ( [m,k] in Indices M & [i,j] in Indices M & (f1 ^ f2) /. n = M * (m,k) & (f1 ^ f2) /. (n + 1) = M * (i,j) implies |.(m - i).| + |.(k - j).| = 1 )
assume that
A6:
( [m,k] in Indices M & [i,j] in Indices M )
and
A7:
(f1 ^ f2) /. n = M * (m,k)
and
A8:
(f1 ^ f2) /. (n + 1) = M * (i,j)
; |.(m - i).| + |.(k - j).| = 1
A9:
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:25;
suppose A10:
n in dom f1
;
|.(m - i).| + |.(k - j).| = 1then A11:
f1 /. n = M * (
m,
k)
by A7, FINSEQ_4:68;
now |.(m - i).| + |.(k - j).| = 1per cases
( n + 1 in dom f1 or ex m being Nat st
( m in dom f2 & n + 1 = (len f1) + m ) )
by A5, FINSEQ_1:25;
suppose
ex
m being
Nat st
(
m in dom f2 &
n + 1
= (len f1) + m )
;
|.(m - i).| + |.(k - j).| = 1then consider mm being
Nat such that A13:
mm in dom f2
and A14:
n + 1
= (len f1) + mm
;
1
<= mm
by A13, FINSEQ_3:25;
then A15:
0 <= mm - 1
by XREAL_1:48;
(len f1) + (mm - 1) <= (len f1) + 0
by A9, A10, A14, FINSEQ_1:1;
then A16:
mm - 1
= 0
by A15, XREAL_1:6;
then
(
M * (
i,
j)
= f2 /. 1 &
M * (
m,
k)
= f1 /. (len f1) )
by A7, A8, A10, A13, A14, FINSEQ_4:68, FINSEQ_4:69;
hence
|.(m - i).| + |.(k - j).| = 1
by A3, A6, A10, A13, A14, A16;
verum end; hence
|.(m - i).| + |.(k - j).| = 1
;
verum end; suppose
ex
m being
Nat st
(
m in dom f2 &
n = (len f1) + m )
;
|.(m - i).| + |.(k - j).| = 1then consider mm being
Nat such that A17:
mm in dom f2
and A18:
n = (len f1) + mm
;
A19:
M * (
m,
k)
= f2 /. mm
by A7, A17, A18, FINSEQ_4:69;
A20:
((len f1) + mm) + 1
= (len f1) + (mm + 1)
;
n + 1
<= len (f1 ^ f2)
by A5, FINSEQ_3:25;
then
((len f1) + mm) + 1
<= (len f1) + (len f2)
by A18, FINSEQ_1:22;
then
( 1
<= mm + 1 &
mm + 1
<= len f2 )
by A20, NAT_1:11, XREAL_1:6;
then A21:
mm + 1
in dom f2
by FINSEQ_3:25;
M * (
i,
j) =
(f1 ^ f2) /. ((len f1) + (mm + 1))
by A8, A18
.=
f2 /. (mm + 1)
by A21, FINSEQ_4:69
;
hence
|.(m - i).| + |.(k - j).| = 1
by A2, A6, A17, A21, A19;
verum end;