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 that
A4: n in dom (f1 ^ f2) and
A5: 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 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: (abs (m - i)) + (abs (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:38;

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

then A11: f1 /. n = M * m,k by A7, 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 A5, FINSEQ_1:38;

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

then f1 /. (n + 1) = M * i,j by A8, FINSEQ_4:83;
hence (abs (m - i)) + (abs (k - j)) = 1 by A1, A6, A10, A11, A12; :: thesis: verum

end;

suppose ex m being Nat st
( m in dom f2 & n + 1 = (len f1) + m ) ; :: thesis: (abs (m - i)) + (abs (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:27;
then A15: 0 <= mm - 1 by XREAL_1:50;
(len f1) + (mm - 1) <= (len f1) + 0 by A9, A10, A14, FINSEQ_1:3;
then A16: mm - 1 = 0 by A15, XREAL_1:8;
then ( M * i,j = f2 /. 1 & M * m,k = f1 /. (len f1) ) by A7, A8, A10, A13, A14, FINSEQ_4:83, FINSEQ_4:84;
hence (abs (m - i)) + (abs (k - j)) = 1 by A3, A6, A10, A13, A14, A16; :: thesis: verum

end;

end;

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)) = 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:84;
A20: ((len f1) + mm) + 1 = (len f1) + (mm + 1) ;
n + 1 <= len (f1 ^ f2) by A5, FINSEQ_3:27;
then ((len f1) + mm) + 1 <= (len f1) + (len f2) by A18, FINSEQ_1:35;
then ( 1 <= mm + 1 & mm + 1 <= len f2 ) by A20, NAT_1:11, XREAL_1:8;
then A21: mm + 1 in dom f2 by FINSEQ_3:27;
M * i,j = (f1 ^ f2) /. ((len f1) + (mm + 1)) by A8, A18
.= f2 /. (mm + 1) by A21, FINSEQ_4:84 ;
hence (abs (m - i)) + (abs (k - j)) = 1 by A2, A6, A17, A21, A19; :: thesis: verum

end;

end;