let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: 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 ; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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; :: 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 |.(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) ; :: thesis: |.(m - i).| + |.(k - j).| = 1

A9: dom f1 = Seg (len f1) by FINSEQ_1:def 3;

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 ; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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; :: 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 |.(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) ; :: thesis: |.(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;

end;

( m in dom f2 & n = (len f1) + m ) ) by A4, FINSEQ_1:25;

suppose A10:
n in dom f1
; :: thesis: |.(m - i).| + |.(k - j).| = 1

then A11:
f1 /. n = M * (m,k)
by A7, FINSEQ_4:68;

end;now :: thesis: |.(m - i).| + |.(k - j).| = 1end;

hence
|.(m - i).| + |.(k - j).| = 1
; :: thesis: verumper 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;

end;

( m in dom f2 & n + 1 = (len f1) + m ) ) by A5, FINSEQ_1:25;

suppose A12:
n + 1 in dom f1
; :: thesis: |.(m - i).| + |.(k - j).| = 1

then
f1 /. (n + 1) = M * (i,j)
by A8, FINSEQ_4:68;

hence |.(m - i).| + |.(k - j).| = 1 by A1, A6, A10, A11, A12; :: thesis: verum

end;hence |.(m - i).| + |.(k - j).| = 1 by A1, A6, A10, A11, A12; :: thesis: verum

suppose
ex m being Nat st

( m in dom f2 & n + 1 = (len f1) + m ) ; :: thesis: |.(m - i).| + |.(k - j).| = 1

( m in dom f2 & n + 1 = (len f1) + m ) ; :: thesis: |.(m - i).| + |.(k - j).| = 1

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

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

suppose
ex m being Nat st

( m in dom f2 & n = (len f1) + m ) ; :: thesis: |.(m - i).| + |.(k - j).| = 1

( m in dom f2 & n = (len f1) + m ) ; :: thesis: |.(m - i).| + |.(k - j).| = 1

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

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