let D be non empty set ; for M being Matrix of D
for f being FinSequence of D
for g being non empty FinSequence of D st f /. (len f) = g /. 1 & f is_sequence_on M & g is_sequence_on M holds
f ^' g is_sequence_on M
let M be Matrix of D; for f being FinSequence of D
for g being non empty FinSequence of D st f /. (len f) = g /. 1 & f is_sequence_on M & g is_sequence_on M holds
f ^' g is_sequence_on M
let f be FinSequence of D; for g being non empty FinSequence of D st f /. (len f) = g /. 1 & f is_sequence_on M & g is_sequence_on M holds
f ^' g is_sequence_on M
let g be non empty FinSequence of D; ( f /. (len f) = g /. 1 & f is_sequence_on M & g is_sequence_on M implies f ^' g is_sequence_on M )
assume that
A1:
f /. (len f) = g /. 1
and
A2:
f is_sequence_on M
and
A3:
g is_sequence_on M
; f ^' g is_sequence_on M
A4:
(len (f ^' g)) + 1 = (len f) + (len g)
by FINSEQ_6:139;
thus
for n being Nat st n in dom (f ^' g) holds
ex i, j being Nat st
( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) )
GOBOARD1:def 9 for b1 being set holds
( not b1 in dom (f ^' g) or not b1 + 1 in dom (f ^' g) or for b2, b3, b4, b5 being set holds
( not [b2,b3] in Indices M or not [b4,b5] in Indices M or not (f ^' g) /. b1 = M * (b2,b3) or not (f ^' g) /. (b1 + 1) = M * (b4,b5) or K187((b2 - b4)) + K187((b3 - b5)) = 1 ) )proof
let n be
Nat;
( n in dom (f ^' g) implies ex i, j being Nat st
( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) ) )
assume A5:
n in dom (f ^' g)
;
ex i, j being Nat st
( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) )
per cases
( n <= len f or n > len f )
;
suppose A6:
n <= len f
;
ex i, j being Nat st
( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) )A7:
1
<= n
by A5, FINSEQ_3:25;
then
n in dom f
by A6, FINSEQ_3:25;
then consider i,
j being
Nat such that A8:
[i,j] in Indices M
and A9:
f /. n = M * (
i,
j)
by A2;
take
i
;
ex j being Nat st
( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) )take
j
;
( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) )thus
[i,j] in Indices M
by A8;
(f ^' g) /. n = M * (i,j)thus
(f ^' g) /. n = M * (
i,
j)
by A6, A7, A9, FINSEQ_6:159;
verum end; suppose A10:
n > len f
;
ex i, j being Nat st
( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) )then consider k being
Nat such that A11:
n = (len f) + k
by NAT_1:10;
reconsider k =
k as
Nat ;
A12:
1
<= k + 1
by NAT_1:11;
n <= len (f ^' g)
by A5, FINSEQ_3:25;
then
n < (len f) + (len g)
by A4, NAT_1:13;
then A13:
k < len g
by A11, XREAL_1:6;
then
k + 1
<= len g
by NAT_1:13;
then
k + 1
in dom g
by A12, FINSEQ_3:25;
then consider i,
j being
Nat such that A14:
[i,j] in Indices M
and A15:
g /. (k + 1) = M * (
i,
j)
by A3;
take
i
;
ex j being Nat st
( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) )take
j
;
( [i,j] in Indices M & (f ^' g) /. n = M * (i,j) )thus
[i,j] in Indices M
by A14;
(f ^' g) /. n = M * (i,j)
(len f) + 1
<= n
by A10, NAT_1:13;
then
1
<= k
by A11, XREAL_1:6;
hence
(f ^' g) /. n = M * (
i,
j)
by A11, A13, A15, FINSEQ_6:160;
verum end;
end;
let n be Nat; ( not n in dom (f ^' g) or not n + 1 in dom (f ^' g) or for b1, b2, b3, b4 being set holds
( not [b1,b2] in Indices M or not [b3,b4] in Indices M or not (f ^' g) /. n = M * (b1,b2) or not (f ^' g) /. (n + 1) = M * (b3,b4) or K187((b1 - b3)) + K187((b2 - b4)) = 1 ) )
assume that
A16:
n in dom (f ^' g)
and
A17:
n + 1 in dom (f ^' g)
; for b1, b2, b3, b4 being set holds
( not [b1,b2] in Indices M or not [b3,b4] in Indices M or not (f ^' g) /. n = M * (b1,b2) or not (f ^' g) /. (n + 1) = M * (b3,b4) or K187((b1 - b3)) + K187((b2 - b4)) = 1 )
let m, k, i, j be Nat; ( not [m,k] in Indices M or not [i,j] in Indices M or not (f ^' g) /. n = M * (m,k) or not (f ^' g) /. (n + 1) = M * (i,j) or K187((m - i)) + K187((k - j)) = 1 )
assume that
A18:
[m,k] in Indices M
and
A19:
[i,j] in Indices M
and
A20:
(f ^' g) /. n = M * (m,k)
and
A21:
(f ^' g) /. (n + 1) = M * (i,j)
; K187((m - i)) + K187((k - j)) = 1
per cases
( n < len f or n > len f or n = len f )
by XXREAL_0:1;
suppose A22:
n < len f
;
K187((m - i)) + K187((k - j)) = 1then A23:
n + 1
<= len f
by NAT_1:13;
then A24:
f /. (n + 1) = M * (
i,
j)
by A21, FINSEQ_6:159, NAT_1:11;
A25:
1
<= n
by A16, FINSEQ_3:25;
then A26:
n in dom f
by A22, FINSEQ_3:25;
1
<= n + 1
by NAT_1:11;
then A27:
n + 1
in dom f
by A23, FINSEQ_3:25;
f /. n = M * (
m,
k)
by A20, A22, A25, FINSEQ_6:159;
hence
K187(
(m - i))
+ K187(
(k - j))
= 1
by A2, A18, A19, A26, A27, A24;
verum end; suppose A28:
n > len f
;
K187((m - i)) + K187((k - j)) = 1then consider k0 being
Nat such that A29:
n = (len f) + k0
by NAT_1:10;
reconsider k0 =
k0 as
Nat ;
A30:
1
<= k0 + 1
by NAT_1:11;
n <= len (f ^' g)
by A16, FINSEQ_3:25;
then
n < (len f) + (len g)
by A4, NAT_1:13;
then A31:
k0 < len g
by A29, XREAL_1:6;
then
k0 + 1
<= len g
by NAT_1:13;
then A32:
k0 + 1
in dom g
by A30, FINSEQ_3:25;
A33:
1
<= (k0 + 1) + 1
by NAT_1:11;
n + 1
<= len (f ^' g)
by A17, FINSEQ_3:25;
then
(len f) + (k0 + 1) < (len f) + (len g)
by A4, A29, NAT_1:13;
then A34:
k0 + 1
< len g
by XREAL_1:6;
then
(k0 + 1) + 1
<= len g
by NAT_1:13;
then A35:
(k0 + 1) + 1
in dom g
by A33, FINSEQ_3:25;
(len f) + 1
<= n
by A28, NAT_1:13;
then
1
<= k0
by A29, XREAL_1:6;
then A36:
g /. (k0 + 1) = M * (
m,
k)
by A20, A29, A31, FINSEQ_6:160;
g /. ((k0 + 1) + 1) =
(f ^' g) /. ((len f) + (k0 + 1))
by A34, FINSEQ_6:160, NAT_1:11
.=
M * (
i,
j)
by A21, A29
;
hence
K187(
(m - i))
+ K187(
(k - j))
= 1
by A3, A18, A19, A32, A35, A36;
verum end; suppose A37:
n = len f
;
K187((m - i)) + K187((k - j)) = 1
n + 1
<= len (f ^' g)
by A17, FINSEQ_3:25;
then
(len f) + 1
< (len f) + (len g)
by A4, A37, NAT_1:13;
then A38:
1
< len g
by XREAL_1:6;
then
1
+ 1
<= len g
by NAT_1:13;
then A39:
1
+ 1
in dom g
by FINSEQ_3:25;
1
<= n
by A16, FINSEQ_3:25;
then A40:
g /. 1
= M * (
m,
k)
by A1, A20, A37, FINSEQ_6:159;
A41:
1
in dom g
by FINSEQ_5:6;
g /. (1 + 1) = M * (
i,
j)
by A21, A37, A38, FINSEQ_6:160;
hence
K187(
(m - i))
+ K187(
(k - j))
= 1
by A3, A18, A19, A40, A39, A41;
verum end;