defpred S1[ Nat] means for G1 being Go-board
for g1, g2 being FinSequence of (TOP-REAL 2) st $1 = width G1 & $1 > 0 & 1 <= len g1 & 1 <= len g2 & g1 is_sequence_on G1 & g2 is_sequence_on G1 & g1 /. 1 in rng (Line (G1,1)) & g1 /. (len g1) in rng (Line (G1,(len G1))) & g2 /. 1 in rng (Col (G1,1)) & g2 /. (len g2) in rng (Col (G1,(width G1))) holds
(rng g1) /\ (rng g2) <> {} ;
let G be Go-board; for f1, f2 being FinSequence of (TOP-REAL 2) st 1 <= len f1 & 1 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) holds
rng f1 meets rng f2
let f1, f2 be FinSequence of (TOP-REAL 2); ( 1 <= len f1 & 1 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) implies rng f1 meets rng f2 )
A1:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A2:
S1[
k]
;
S1[k + 1]
let G1 be
Go-board;
for g1, g2 being FinSequence of (TOP-REAL 2) st k + 1 = width G1 & k + 1 > 0 & 1 <= len g1 & 1 <= len g2 & g1 is_sequence_on G1 & g2 is_sequence_on G1 & g1 /. 1 in rng (Line (G1,1)) & g1 /. (len g1) in rng (Line (G1,(len G1))) & g2 /. 1 in rng (Col (G1,1)) & g2 /. (len g2) in rng (Col (G1,(width G1))) holds
(rng g1) /\ (rng g2) <> {} let g1,
g2 be
FinSequence of
(TOP-REAL 2);
( k + 1 = width G1 & k + 1 > 0 & 1 <= len g1 & 1 <= len g2 & g1 is_sequence_on G1 & g2 is_sequence_on G1 & g1 /. 1 in rng (Line (G1,1)) & g1 /. (len g1) in rng (Line (G1,(len G1))) & g2 /. 1 in rng (Col (G1,1)) & g2 /. (len g2) in rng (Col (G1,(width G1))) implies (rng g1) /\ (rng g2) <> {} )
assume that A3:
k + 1
= width G1
and
k + 1
> 0
and A4:
1
<= len g1
and A5:
1
<= len g2
and A6:
g1 is_sequence_on G1
and A7:
g2 is_sequence_on G1
and A8:
g1 /. 1
in rng (Line (G1,1))
and A9:
g1 /. (len g1) in rng (Line (G1,(len G1)))
and A10:
g2 /. 1
in rng (Col (G1,1))
and A11:
g2 /. (len g2) in rng (Col (G1,(width G1)))
;
(rng g1) /\ (rng g2) <> {}
defpred S2[
Nat]
means ( $1
in dom g2 &
g2 /. $1
in rng (Col (G1,(width G1))) );
A12:
ex
m being
Nat st
S2[
m]
by A5, A11, FINSEQ_3:25;
consider m being
Nat such that A13:
(
S2[
m] & ( for
i being
Nat st
S2[
i] holds
m <= i ) )
from NAT_1:sch 5(A12);
reconsider m =
m as
Nat ;
set g =
g2 | m;
A14:
(g2 | m) /. 1
in rng (Col (G1,1))
by A10, A13, FINSEQ_4:92;
A15:
g2 | m is_sequence_on G1
by A7, GOBOARD1:22;
A16:
m <= len g2
by A13, FINSEQ_3:25;
then A17:
len (g2 | m) = m
by FINSEQ_1:59;
A18:
rng (g2 | m) c= rng g2
reconsider L1 =
Line (
G1,1),
Ll =
Line (
G1,
(len G1)) as
FinSequence of
(TOP-REAL 2) ;
A23:
dom g2 = Seg (len g2)
by FINSEQ_1:def 3;
A24:
dom (g2 | m) = Seg (len (g2 | m))
by FINSEQ_1:def 3;
0 <> len G1
by MATRIX_0:def 10;
then A25:
0 + 1
<= len G1
by NAT_1:14;
then A26:
1
in dom G1
by FINSEQ_3:25;
A27:
len G1 in dom G1
by A25, FINSEQ_3:25;
A28:
(g2 | m) /. (len (g2 | m)) in rng (Col (G1,(width G1)))
by A13, FINSEQ_4:93;
defpred S3[
Nat]
means ( $1
in dom G1 &
(rng (g2 | m)) /\ (rng (Line (G1,$1))) <> {} );
A29:
for
n being
Nat st
S3[
n] holds
n <= len G1
by FINSEQ_3:25;
0 <> width G1
by MATRIX_0:def 10;
then A30:
0 + 1
<= width G1
by NAT_1:14;
then A31:
1
in Seg (width G1)
by FINSEQ_1:1;
A32:
1
<= len (g2 | m)
by A13, GOBOARD1:22;
then A33:
1
in dom (g2 | m)
by FINSEQ_3:25;
A34:
ex
n being
Nat st
S3[
n]
proof
(
m in dom g2 implies
g2 /. 1
= (g2 | m) /. 1 )
by FINSEQ_4:92;
then consider i being
Nat such that A35:
i in dom (Col (G1,1))
and A36:
(g2 | m) /. 1
= (Col (G1,1)) . i
by A10, A13, FINSEQ_2:10;
reconsider i =
i as
Nat ;
take
i
;
S3[i]
i in Seg (len (Col (G1,1)))
by A35, FINSEQ_1:def 3;
then
i in Seg (len G1)
by MATRIX_0:def 8;
hence
i in dom G1
by FINSEQ_1:def 3;
(rng (g2 | m)) /\ (rng (Line (G1,i))) <> {}
then A37:
(g2 | m) /. 1
= (Line (G1,i)) . 1
by A31, A36, MATRIX_0:42;
A38:
(g2 | m) /. 1
in rng (g2 | m)
by A33, PARTFUN2:2;
len (Line (G1,i)) = width G1
by MATRIX_0:def 7;
then
dom (Line (G1,i)) = Seg (width G1)
by FINSEQ_1:def 3;
then
(g2 | m) /. 1
in rng (Line (G1,i))
by A31, A37, FUNCT_1:def 3;
hence
(rng (g2 | m)) /\ (rng (Line (G1,i))) <> {}
by A38, XBOOLE_0:def 4;
verum
end;
consider mi being
Nat such that A39:
(
S3[
mi] & ( for
n being
Nat st
S3[
n] holds
mi <= n ) )
from NAT_1:sch 5(A34);
A40:
ex
n being
Nat st
S3[
n]
by A34;
consider ma being
Nat such that A41:
(
S3[
ma] & ( for
n being
Nat st
S3[
n] holds
n <= ma ) )
from NAT_1:sch 6(A29, A40);
reconsider mi =
mi,
ma =
ma as
Nat ;
A42:
1
<= mi
by A39, FINSEQ_3:25;
reconsider Lmi =
Line (
G1,
mi) as
FinSequence of
(TOP-REAL 2) ;
defpred S4[
Nat]
means ( $1
in dom g1 &
g1 /. $1
in rng (Line (G1,mi)) );
A43:
for
n being
Nat st
S4[
n] holds
n <= len g1
by FINSEQ_3:25;
A44:
mi <= len G1
by A39, FINSEQ_3:25;
then
ex
n being
Nat st
S4[
n]
by A4, A6, A8, A9, A42, GOBOARD1:29;
then A45:
ex
n being
Nat st
S4[
n]
;
consider ma1 being
Nat such that A46:
(
S4[
ma1] & ( for
n being
Nat st
S4[
n] holds
n <= ma1 ) )
from NAT_1:sch 6(A43, A45);
A47:
ma <= len G1
by A41, FINSEQ_3:25;
1
<= mi
by A39, FINSEQ_3:25;
then reconsider l1 =
mi - 1,
l2 =
(len G1) - ma as
Element of
NAT by A47, INT_1:5;
A48:
ma <= len G1
by A41, FINSEQ_3:25;
reconsider ma1 =
ma1 as
Nat ;
consider k1 being
Element of
NAT such that A49:
k1 in dom Lmi
and A50:
g1 /. ma1 = Lmi /. k1
by A46, PARTFUN2:2;
Seg (len Lmi) = dom Lmi
by FINSEQ_1:def 3;
then A51:
k1 in Seg (width G1)
by A49, MATRIX_0:def 7;
A52:
dom G1 = Seg (len G1)
by FINSEQ_1:def 3;
A53:
(
mi = ma implies
(rng g1) /\ (rng g2) <> {} )
proof
consider n being
Nat such that A54:
n in dom g1
and A55:
g1 /. n in rng (Line (G1,mi))
by A4, A6, A8, A9, A42, A44, GOBOARD1:29;
consider i being
Element of
NAT such that A56:
i in dom (Line (G1,mi))
and A57:
g1 /. n = Lmi /. i
by A55, PARTFUN2:2;
A58:
1
<= i
by A56, FINSEQ_3:25;
A59:
len (Line (G1,mi)) = width G1
by MATRIX_0:def 7;
then
i <= width G1
by A56, FINSEQ_3:25;
then consider m being
Nat such that A60:
m in dom (g2 | m)
and A61:
(g2 | m) /. m in rng (Col (G1,i))
by A32, A15, A14, A28, A58, GOBOARD1:33;
A62:
(g2 | m) /. m in rng (g2 | m)
by A60, PARTFUN2:2;
reconsider Ci =
Col (
G1,
i) as
FinSequence of
(TOP-REAL 2) ;
A63:
len (Col (G1,i)) = len G1
by MATRIX_0:def 8;
then A64:
dom (Col (G1,i)) =
Seg (len G1)
by FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
assume A65:
mi = ma
;
(rng g1) /\ (rng g2) <> {}
A66:
dom (Line (G1,mi)) = Seg (len (Line (G1,mi)))
by FINSEQ_1:def 3;
consider j being
Element of
NAT such that A67:
j in dom Ci
and A68:
(g2 | m) /. m = Ci /. j
by A61, PARTFUN2:2;
reconsider Lj =
Line (
G1,
j) as
FinSequence of
(TOP-REAL 2) ;
len (Line (G1,mi)) =
width G1
by MATRIX_0:def 7
.=
len Lj
by MATRIX_0:def 7
;
then A69:
dom (Line (G1,mi)) = dom Lj
by A66, FINSEQ_1:def 3;
A70:
(g2 | m) /. m =
Ci . j
by A67, A68, PARTFUN1:def 6
.=
Lj . i
by A56, A66, A59, A64, A67, MATRIX_0:42
.=
Lj /. i
by A56, A69, PARTFUN1:def 6
;
len Lj = width G1
by MATRIX_0:def 7;
then
i in dom Lj
by A56, A66, A59, FINSEQ_1:def 3;
then
(g2 | m) /. m in rng Lj
by A70, PARTFUN2:2;
then A71:
(
dom Ci = Seg (len Ci) &
(rng (g2 | m)) /\ (rng (Line (G1,j))) <> {} )
by A62, FINSEQ_1:def 3, XBOOLE_0:def 4;
g1 /. n in rng g1
by A54, PARTFUN2:2;
hence
(rng g1) /\ (rng g2) <> {}
by A18, A57, A62, A70, A72, XBOOLE_0:def 4;
verum
end;
A73:
width G1 in Seg (width G1)
by A30, FINSEQ_1:1;
deffunc H1(
Nat)
-> Element of the
U1 of
(TOP-REAL 2) =
G1 * ($1,
k1);
reconsider Ck1 =
Col (
G1,
k1) as
FinSequence of
(TOP-REAL 2) ;
consider h1 being
FinSequence of
(TOP-REAL 2) such that A74:
(
len h1 = l1 & ( for
n being
Nat st
n in dom h1 holds
h1 /. n = H1(
n) ) )
from FINSEQ_4:sch 2();
A75:
dom g1 = Seg (len g1)
by FINSEQ_1:def 3;
now (rng g1) /\ (rng g2) <> {} per cases
( k = 0 or k <> 0 )
;
suppose A76:
k = 0
;
(rng g1) /\ (rng g2) <> {} reconsider c1 =
Col (
G1,1) as
FinSequence of
(TOP-REAL 2) ;
consider x being
Element of
NAT such that A77:
x in dom c1
and A78:
g2 /. 1
= c1 /. x
by A10, PARTFUN2:2;
reconsider lx =
Line (
G1,
x) as
FinSequence of
(TOP-REAL 2) ;
A79:
1
<= x
by A77, FINSEQ_3:25;
A80:
len c1 = len G1
by MATRIX_0:def 8;
then
x <= len G1
by A77, FINSEQ_3:25;
then consider m being
Nat such that A81:
m in dom g1
and A82:
g1 /. m in rng lx
by A4, A6, A8, A9, A79, GOBOARD1:29;
A83:
g1 /. m in rng g1
by A81, PARTFUN2:2;
Seg (len c1) = dom c1
by FINSEQ_1:def 3;
then A84:
x in dom G1
by A77, A80, FINSEQ_1:def 3;
A85:
c1 /. x = c1 . x
by A77, PARTFUN1:def 6;
consider y being
Element of
NAT such that A86:
y in dom lx
and A87:
lx /. y = g1 /. m
by A82, PARTFUN2:2;
(
Seg (len lx) = dom lx &
len lx = width G1 )
by FINSEQ_1:def 3, MATRIX_0:def 7;
then A88:
y = 1
by A3, A76, A86, FINSEQ_1:2, TARSKI:def 1;
0 <> width G1
by MATRIX_0:def 10;
then
0 + 1
<= width G1
by NAT_1:14;
then A89:
1
in Seg (width G1)
by FINSEQ_1:1;
1
in dom g2
by A5, FINSEQ_3:25;
then A90:
g2 /. 1
in rng g2
by PARTFUN2:2;
lx /. y = lx . y
by A86, PARTFUN1:def 6;
then
g1 /. m = g2 /. 1
by A78, A89, A84, A87, A85, A88, MATRIX_0:42;
hence
(rng g1) /\ (rng g2) <> {}
by A83, A90, XBOOLE_0:def 4;
verum end; suppose A91:
k <> 0
;
(rng g1) /\ (rng g2) <> {} then A92:
0 < k
;
then A93:
width G1 > 1
+ 0
by A3, XREAL_1:8;
then A94:
width G1 in Seg (width G1)
by FINSEQ_1:1;
now (rng g1) /\ (rng g2) <> {} per cases
( mi = ma or mi <> ma )
;
suppose A95:
mi <> ma
;
(rng g1) /\ (rng g2) <> {}
1
<= ma1
by A46, FINSEQ_3:25;
then reconsider w =
ma1 - 1 as
Element of
NAT by INT_1:5;
reconsider Lma =
Line (
G1,
ma) as
FinSequence of
(TOP-REAL 2) ;
A96:
Indices G1 = [:(dom G1),(Seg (width G1)):]
by MATRIX_0:def 4;
A102:
now for n being Nat st n in dom h1 & n + 1 in dom h1 holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. n = G1 * (i1,i2) & h1 /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1let n be
Nat;
( n in dom h1 & n + 1 in dom h1 implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. n = G1 * (i1,i2) & h1 /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A103:
n in dom h1
and A104:
n + 1
in dom h1
;
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. n = G1 * (i1,i2) & h1 /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
n + 1
in dom G1
by A97, A104;
then A105:
[(n + 1),k1] in Indices G1
by A51, A96, ZFMISC_1:87;
let i1,
i2,
j1,
j2 be
Nat;
( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. n = G1 * (i1,i2) & h1 /. (n + 1) = G1 * (j1,j2) implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A106:
[i1,i2] in Indices G1
and A107:
[j1,j2] in Indices G1
and A108:
h1 /. n = G1 * (
i1,
i2)
and A109:
h1 /. (n + 1) = G1 * (
j1,
j2)
;
|.(i1 - j1).| + |.(i2 - j2).| = 1
h1 /. (n + 1) = G1 * (
(n + 1),
k1)
by A74, A104;
then A110:
(
j1 = n + 1 &
j2 = k1 )
by A105, A107, A109, GOBOARD1:5;
n in dom G1
by A97, A103;
then A111:
[n,k1] in Indices G1
by A51, A96, ZFMISC_1:87;
h1 /. n = G1 * (
n,
k1)
by A74, A103;
then
(
i1 = n &
i2 = k1 )
by A111, A106, A108, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| =
|.((n - n) + (- 1)).| + 0
by A110, ABSVALUE:2
.=
|.1.|
by COMPLEX1:52
.=
1
by ABSVALUE:def 1
;
verum end; A112:
(rng h1) /\ (rng (g2 | m)) = {}
proof
set x = the
Element of
(rng h1) /\ (rng (g2 | m));
assume A113:
not
(rng h1) /\ (rng (g2 | m)) = {}
;
contradiction
then
the
Element of
(rng h1) /\ (rng (g2 | m)) in rng h1
by XBOOLE_0:def 4;
then consider n1 being
Element of
NAT such that A114:
n1 in dom h1
and A115:
the
Element of
(rng h1) /\ (rng (g2 | m)) = h1 /. n1
by PARTFUN2:2;
A116:
n1 <= l1
by A74, A114, FINSEQ_3:25;
n1 in dom G1
by A97, A114;
then A117:
[n1,k1] in Indices G1
by A51, A96, ZFMISC_1:87;
the
Element of
(rng h1) /\ (rng (g2 | m)) in rng (g2 | m)
by A113, XBOOLE_0:def 4;
then consider n2 being
Element of
NAT such that A118:
n2 in dom (g2 | m)
and A119:
the
Element of
(rng h1) /\ (rng (g2 | m)) = (g2 | m) /. n2
by PARTFUN2:2;
A120:
(g2 | m) /. n2 in rng (g2 | m)
by A118, PARTFUN2:2;
consider i1,
i2 being
Nat such that A121:
[i1,i2] in Indices G1
and A122:
(g2 | m) /. n2 = G1 * (
i1,
i2)
by A15, A118, GOBOARD1:def 9;
reconsider L =
Line (
G1,
i1) as
FinSequence of
(TOP-REAL 2) ;
A123:
i2 in Seg (width G1)
by A96, A121, ZFMISC_1:87;
A124:
(
Seg (len L) = dom L &
len L = width G1 )
by FINSEQ_1:def 3, MATRIX_0:def 7;
then
L /. i2 = L . i2
by A123, PARTFUN1:def 6;
then
(g2 | m) /. n2 = L /. i2
by A122, A123, MATRIX_0:def 7;
then
(g2 | m) /. n2 in rng L
by A123, A124, PARTFUN2:2;
then A125:
(rng (g2 | m)) /\ (rng L) <> {}
by A120, XBOOLE_0:def 4;
i1 in dom G1
by A96, A121, ZFMISC_1:87;
then A126:
mi <= i1
by A39, A125;
the
Element of
(rng h1) /\ (rng (g2 | m)) = G1 * (
n1,
k1)
by A74, A114, A115;
then
i1 = n1
by A119, A121, A122, A117, GOBOARD1:5;
then
mi <= mi - 1
by A116, A126, XXREAL_0:2;
hence
contradiction
by XREAL_1:44;
verum
end; defpred S5[
Nat]
means ( $1
in dom g1 &
ma1 < $1 &
g1 /. $1
in rng (Line (G1,ma)) );
A127:
mi <= ma
by A39, A41;
then A128:
mi < ma
by A95, XXREAL_0:1;
then
ex
n being
Nat st
S5[
n]
by A6, A9, A39, A48, A46, GOBOARD1:37;
then A129:
ex
n being
Nat st
S5[
n]
;
consider mi1 being
Nat such that A130:
(
S5[
mi1] & ( for
n being
Nat st
S5[
n] holds
mi1 <= n ) )
from NAT_1:sch 5(A129);
consider k2 being
Element of
NAT such that A131:
k2 in dom Lma
and A132:
g1 /. mi1 = Lma /. k2
by A130, PARTFUN2:2;
deffunc H2(
Nat)
-> Element of the
U1 of
(TOP-REAL 2) =
G1 * (
(ma + $1),
k2);
consider h2 being
FinSequence of
(TOP-REAL 2) such that A133:
(
len h2 = l2 & ( for
n being
Nat st
n in dom h2 holds
h2 /. n = H2(
n) ) )
from FINSEQ_4:sch 2();
reconsider Ck2 =
Col (
G1,
k2) as
FinSequence of
(TOP-REAL 2) ;
dom Lma = Seg (len Lma)
by FINSEQ_1:def 3;
then A134:
k2 in Seg (width G1)
by A131, MATRIX_0:def 7;
A139:
now for n being Nat st n in dom h2 holds
ex m, k2 being Nat st
( [m,k2] in Indices G1 & h2 /. n = G1 * (m,k2) )let n be
Nat;
( n in dom h2 implies ex m, k2 being Nat st
( [m,k2] in Indices G1 & h2 /. n = G1 * (m,k2) ) )assume A140:
n in dom h2
;
ex m, k2 being Nat st
( [m,k2] in Indices G1 & h2 /. n = G1 * (m,k2) )reconsider m =
ma + n,
k2 =
k2 as
Nat ;
take m =
m;
ex k2 being Nat st
( [m,k2] in Indices G1 & h2 /. n = G1 * (m,k2) )take k2 =
k2;
( [m,k2] in Indices G1 & h2 /. n = G1 * (m,k2) )
ma + n in dom G1
by A135, A140;
hence
(
[m,k2] in Indices G1 &
h2 /. n = G1 * (
m,
k2) )
by A134, A133, A96, A140, ZFMISC_1:87;
verum end; A141:
now for n being Nat st n in dom h2 & n + 1 in dom h2 holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h2 /. n = G1 * (i1,i2) & h2 /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1let n be
Nat;
( n in dom h2 & n + 1 in dom h2 implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h2 /. n = G1 * (i1,i2) & h2 /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A142:
n in dom h2
and A143:
n + 1
in dom h2
;
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h2 /. n = G1 * (i1,i2) & h2 /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
ma + (n + 1) in dom G1
by A135, A143;
then A144:
[((ma + n) + 1),k2] in Indices G1
by A134, A96, ZFMISC_1:87;
let i1,
i2,
j1,
j2 be
Nat;
( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h2 /. n = G1 * (i1,i2) & h2 /. (n + 1) = G1 * (j1,j2) implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A145:
[i1,i2] in Indices G1
and A146:
[j1,j2] in Indices G1
and A147:
h2 /. n = G1 * (
i1,
i2)
and A148:
h2 /. (n + 1) = G1 * (
j1,
j2)
;
|.(i1 - j1).| + |.(i2 - j2).| = 1
h2 /. (n + 1) = G1 * (
(ma + (n + 1)),
k2)
by A133, A143;
then A149:
(
j1 = (ma + n) + 1 &
j2 = k2 )
by A144, A146, A148, GOBOARD1:5;
ma + n in dom G1
by A135, A142;
then A150:
[(ma + n),k2] in Indices G1
by A134, A96, ZFMISC_1:87;
h2 /. n = G1 * (
(ma + n),
k2)
by A133, A142;
then
(
i1 = ma + n &
i2 = k2 )
by A150, A145, A147, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| =
|.(((ma + n) - (ma + n)) + (- 1)).| + 0
by A149, ABSVALUE:2
.=
|.1.|
by COMPLEX1:52
.=
1
by ABSVALUE:def 1
;
verum end; A151:
mi1 <= mi1 + 1
by NAT_1:11;
A152:
0 + 1
< width G1
by A3, A92, XREAL_1:6;
A153:
len (DelCol (G1,(width G1))) = len G1
by MATRIX_0:def 13;
ma1 <= mi1
by A130;
then reconsider l =
(mi1 + 1) - ma1 as
Element of
NAT by A151, INT_1:5, XXREAL_0:2;
set f1 =
g1 | mi1;
defpred S6[
Nat,
Element of
(TOP-REAL 2)]
means $2
= (g1 | mi1) /. (w + $1);
A154:
for
n being
Nat st
n in Seg l holds
ex
p being
Point of
(TOP-REAL 2) st
S6[
n,
p]
;
consider f being
FinSequence of
(TOP-REAL 2) such that A155:
(
len f = l & ( for
n being
Nat st
n in Seg l holds
S6[
n,
f /. n] ) )
from FINSEQ_4:sch 1(A154);
A156:
w + l = mi1
;
A157:
dom f = Seg l
by A155, FINSEQ_1:def 3;
set ff =
(h1 ^ f) ^ h2;
ma1 + 1
<= mi1
by A130, NAT_1:13;
then
ma1 + 1
<= mi1 + 1
by NAT_1:13;
then A158:
1
<= l
by XREAL_1:19;
A159:
now ((h1 ^ f) ^ h2) /. 1 in rng (Line (G1,1))per cases
( mi = 1 or mi <> 1 )
;
suppose A160:
mi = 1
;
((h1 ^ f) ^ h2) /. 1 in rng (Line (G1,1))
1
<= ma1
by A75, A46, FINSEQ_1:1;
then A161:
ma1 in Seg mi1
by A130, FINSEQ_1:1;
A162:
w + 1
= ma1
;
A163:
1
in Seg l
by A158, FINSEQ_1:1;
h1 = {}
by A74, A160;
then
(h1 ^ f) ^ h2 = f ^ h2
by FINSEQ_1:34;
then ((h1 ^ f) ^ h2) /. 1 =
f /. 1
by A157, A163, FINSEQ_4:68
.=
(g1 | mi1) /. ma1
by A155, A163, A162
.=
g1 /. ma1
by A130, A161, FINSEQ_4:71
;
hence
((h1 ^ f) ^ h2) /. 1
in rng (Line (G1,1))
by A46, A160;
verum end; suppose A164:
mi <> 1
;
((h1 ^ f) ^ h2) /. 1 in rng (Line (G1,1))
1
<= mi
by A39, FINSEQ_3:25;
then
1
< mi
by A164, XXREAL_0:1;
then
1
+ 1
<= mi
by NAT_1:13;
then A165:
1
<= l1
by XREAL_1:19;
then A166:
1
in dom h1
by A74, FINSEQ_3:25;
A167:
len (Line (G1,1)) = width G1
by MATRIX_0:def 7;
then A168:
k1 in dom L1
by A51, FINSEQ_1:def 3;
dom (Line (G1,1)) = Seg (width G1)
by A167, FINSEQ_1:def 3;
then A169:
L1 /. k1 = L1 . k1
by A51, PARTFUN1:def 6;
(
len (h1 ^ f) = (len h1) + (len f) &
0 <= len f )
by FINSEQ_1:22;
then
0 + 1
<= len (h1 ^ f)
by A74, A165, XREAL_1:7;
then
1
in dom (h1 ^ f)
by FINSEQ_3:25;
then ((h1 ^ f) ^ h2) /. 1 =
(h1 ^ f) /. 1
by FINSEQ_4:68
.=
h1 /. 1
by A166, FINSEQ_4:68
.=
G1 * (1,
k1)
by A74, A166
.=
L1 /. k1
by A51, A169, MATRIX_0:def 7
;
hence
((h1 ^ f) ^ h2) /. 1
in rng (Line (G1,1))
by A168, PARTFUN2:2;
verum end; end; end; A170:
for
n being
Nat st
n in Seg l holds
(
(g1 | mi1) /. (w + n) = g1 /. (w + n) &
w + n in dom g1 )
A174:
now for n being Nat st n in dom f holds
ex i, j being Nat st
( [i,j] in Indices G1 & f /. n = G1 * (i,j) )let n be
Nat;
( n in dom f implies ex i, j being Nat st
( [i,j] in Indices G1 & f /. n = G1 * (i,j) ) )assume A175:
n in dom f
;
ex i, j being Nat st
( [i,j] in Indices G1 & f /. n = G1 * (i,j) )then
w + n in dom g1
by A170, A157;
then consider i,
j being
Nat such that A176:
(
[i,j] in Indices G1 &
g1 /. (w + n) = G1 * (
i,
j) )
by A6, GOBOARD1:def 9;
take i =
i;
ex j being Nat st
( [i,j] in Indices G1 & f /. n = G1 * (i,j) )take j =
j;
( [i,j] in Indices G1 & f /. n = G1 * (i,j) )
f /. n = (g1 | mi1) /. (w + n)
by A155, A157, A175;
hence
(
[i,j] in Indices G1 &
f /. n = G1 * (
i,
j) )
by A170, A157, A175, A176;
verum end; A177:
Seg (len f) = dom f
by FINSEQ_1:def 3;
A178:
rng f c= rng g1
proof
let x be
object ;
TARSKI:def 3 ( not x in rng f or x in rng g1 )
assume
x in rng f
;
x in rng g1
then consider n being
Element of
NAT such that A179:
n in dom f
and A180:
x = f /. n
by PARTFUN2:2;
f /. n = (g1 | mi1) /. (w + n)
by A155, A177, A179;
then A181:
f /. n = g1 /. (w + n)
by A170, A155, A177, A179;
w + n in dom g1
by A170, A155, A177, A179;
hence
x in rng g1
by A180, A181, PARTFUN2:2;
verum
end; A182:
dom h2 = Seg (len h2)
by FINSEQ_1:def 3;
A183:
now ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line (G1,(len G1)))per cases
( ma = len G1 or ma <> len G1 )
;
suppose A184:
ma = len G1
;
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line (G1,(len G1)))
1
<= mi1
by A130, FINSEQ_3:25;
then A185:
mi1 in Seg mi1
by FINSEQ_1:1;
A186:
len f in dom f
by A155, A177, A158, FINSEQ_1:1;
h2 = {}
by A133, A184;
then A187:
(h1 ^ f) ^ h2 = h1 ^ f
by FINSEQ_1:34;
then ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) =
((h1 ^ f) ^ h2) /. ((len h1) + (len f))
by FINSEQ_1:22
.=
f /. l
by A155, A187, A186, FINSEQ_4:69
.=
(g1 | mi1) /. mi1
by A155, A157, A156, A186
.=
g1 /. mi1
by A130, A185, FINSEQ_4:71
;
hence
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line (G1,(len G1)))
by A130, A184;
verum end; suppose A188:
ma <> len G1
;
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line (G1,(len G1)))
ma <= len G1
by A41, FINSEQ_3:25;
then
ma < len G1
by A188, XXREAL_0:1;
then
ma + 1
<= len G1
by NAT_1:13;
then A189:
1
<= l2
by XREAL_1:19;
then A190:
l2 in Seg l2
by FINSEQ_1:1;
A191:
len h2 in dom h2
by A133, A189, FINSEQ_3:25;
A192:
len (Line (G1,(len G1))) = width G1
by MATRIX_0:def 7;
then A193:
k2 in dom Ll
by A134, FINSEQ_1:def 3;
k2 in dom Ll
by A134, A192, FINSEQ_1:def 3;
then A194:
Ll /. k2 = Ll . k2
by PARTFUN1:def 6;
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) =
((h1 ^ f) ^ h2) /. ((len (h1 ^ f)) + (len h2))
by FINSEQ_1:22
.=
h2 /. l2
by A133, A191, FINSEQ_4:69
.=
G1 * (
(ma + l2),
k2)
by A133, A182, A190
.=
Ll /. k2
by A134, A194, MATRIX_0:def 7
;
hence
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line (G1,(len G1)))
by A193, PARTFUN2:2;
verum end; end; end; A195:
0 + 1
<= (len f) + ((len h1) + (len h2))
by A155, A158, XREAL_1:7;
A196:
rng ((h1 ^ f) ^ h2) =
(rng (h1 ^ f)) \/ (rng h2)
by FINSEQ_1:31
.=
((rng h1) \/ (rng f)) \/ (rng h2)
by FINSEQ_1:31
;
A197:
for
k being
Nat st
k in Seg (width G1) &
(rng f) /\ (rng (Col (G1,k))) = {} holds
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = {}
proof
A198:
len (Col (G1,k2)) = len G1
by MATRIX_0:def 8;
A199:
len (Col (G1,k1)) = len G1
by MATRIX_0:def 8;
A200:
w + 1
= ma1
;
let k be
Nat;
( k in Seg (width G1) & (rng f) /\ (rng (Col (G1,k))) = {} implies (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = {} )
assume that A201:
k in Seg (width G1)
and A202:
(rng f) /\ (rng (Col (G1,k))) = {}
;
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = {}
set gg =
Col (
G1,
k);
assume A203:
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) <> {}
;
contradiction
set x = the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k)));
rng ((h1 ^ f) ^ h2) = (rng f) \/ ((rng h1) \/ (rng h2))
by A196, XBOOLE_1:4;
then A204:
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) =
{} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col (G1,k))))
by A202, XBOOLE_1:23
.=
((rng h1) /\ (rng (Col (G1,k)))) \/ ((rng h2) /\ (rng (Col (G1,k))))
by XBOOLE_1:23
;
now contradictionper cases
( the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k))) or the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k))) )
by A203, A204, XBOOLE_0:def 3;
suppose A205:
the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k)))
;
contradictionthen
the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in rng h1
by XBOOLE_0:def 4;
then consider i being
Element of
NAT such that A206:
i in dom h1
and A207:
the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = h1 /. i
by PARTFUN2:2;
A208:
the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = G1 * (
i,
k1)
by A74, A206, A207;
reconsider y = the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) as
Point of
(TOP-REAL 2) by A207;
A209:
Lmi /. k1 = Lmi . k1
by A49, PARTFUN1:def 6;
A210:
the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k))
by A205, XBOOLE_0:def 4;
A211:
dom (Col (G1,k1)) =
Seg (len G1)
by A199, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
then A212:
Ck1 /. mi = Ck1 . mi
by A39, PARTFUN1:def 6;
A213:
i in dom Ck1
by A97, A206, A211;
Ck1 /. i = Ck1 . i
by A97, A206, A211, PARTFUN1:def 6;
then
y = Ck1 /. i
by A208, A211, A213, MATRIX_0:def 8;
then
y in rng Ck1
by A213, PARTFUN2:2;
then A214:
k1 = k
by A51, A201, A210, GOBOARD1:4;
A215:
1
in Seg l
by A158, FINSEQ_1:1;
then
(
f /. 1
= (g1 | mi1) /. ma1 &
(g1 | mi1) /. ma1 = g1 /. (w + 1) )
by A170, A155, A200;
then
f /. 1
= Ck1 /. mi
by A39, A50, A51, A209, A212, MATRIX_0:42;
then A216:
f /. 1
in rng (Col (G1,k))
by A39, A211, A214, PARTFUN2:2;
f /. 1
in rng f
by A157, A215, PARTFUN2:2;
hence
contradiction
by A202, A216, XBOOLE_0:def 4;
verum end; suppose A217:
the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k)))
;
contradictionthen
the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in rng h2
by XBOOLE_0:def 4;
then consider i being
Element of
NAT such that A218:
i in dom h2
and A219:
the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = h2 /. i
by PARTFUN2:2;
A220:
the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = G1 * (
(ma + i),
k2)
by A133, A218, A219;
reconsider y = the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) as
Point of
(TOP-REAL 2) by A219;
A221:
Lma /. k2 = Lma . k2
by A131, PARTFUN1:def 6;
A222:
the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k))
by A217, XBOOLE_0:def 4;
A223:
dom (Col (G1,k2)) =
Seg (len G1)
by A198, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
then A224:
Ck2 /. ma = Ck2 . ma
by A41, PARTFUN1:def 6;
A225:
ma + i in dom Ck2
by A135, A218, A223;
Ck2 /. (ma + i) = Ck2 . (ma + i)
by A135, A218, A223, PARTFUN1:def 6;
then
y = Ck2 /. (ma + i)
by A220, A223, A225, MATRIX_0:def 8;
then
y in rng Ck2
by A225, PARTFUN2:2;
then A226:
k2 = k
by A134, A201, A222, GOBOARD1:4;
A227:
l in Seg l
by A158, FINSEQ_1:1;
then
(
f /. l = (g1 | mi1) /. (w + l) &
(g1 | mi1) /. (w + l) = g1 /. (w + l) )
by A170, A155;
then
f /. l = Ck2 /. ma
by A41, A132, A134, A221, A224, MATRIX_0:42;
then A228:
f /. l in rng (Col (G1,k))
by A41, A223, A226, PARTFUN2:2;
f /. l in rng f
by A157, A227, PARTFUN2:2;
hence
contradiction
by A202, A228, XBOOLE_0:def 4;
verum end; end; end;
hence
contradiction
;
verum
end;
(rng h2) /\ (rng (g2 | m)) = {}
proof
set x = the
Element of
(rng h2) /\ (rng (g2 | m));
assume A229:
not
(rng h2) /\ (rng (g2 | m)) = {}
;
contradiction
then
the
Element of
(rng h2) /\ (rng (g2 | m)) in rng h2
by XBOOLE_0:def 4;
then consider n1 being
Element of
NAT such that A230:
n1 in dom h2
and A231:
the
Element of
(rng h2) /\ (rng (g2 | m)) = h2 /. n1
by PARTFUN2:2;
A232:
1
<= n1
by A230, FINSEQ_3:25;
ma + n1 in dom G1
by A135, A230;
then A233:
[(ma + n1),k2] in Indices G1
by A134, A96, ZFMISC_1:87;
the
Element of
(rng h2) /\ (rng (g2 | m)) in rng (g2 | m)
by A229, XBOOLE_0:def 4;
then consider n2 being
Element of
NAT such that A234:
n2 in dom (g2 | m)
and A235:
the
Element of
(rng h2) /\ (rng (g2 | m)) = (g2 | m) /. n2
by PARTFUN2:2;
consider i1,
i2 being
Nat such that A236:
[i1,i2] in Indices G1
and A237:
(g2 | m) /. n2 = G1 * (
i1,
i2)
by A15, A234, GOBOARD1:def 9;
reconsider L =
Line (
G1,
i1) as
FinSequence of
(TOP-REAL 2) ;
A238:
i2 in Seg (width G1)
by A96, A236, ZFMISC_1:87;
A239:
(
Seg (len L) = dom L &
len L = width G1 )
by FINSEQ_1:def 3, MATRIX_0:def 7;
then
L /. i2 = L . i2
by A238, PARTFUN1:def 6;
then
(g2 | m) /. n2 = L /. i2
by A237, A238, MATRIX_0:def 7;
then A240:
(g2 | m) /. n2 in rng L
by A238, A239, PARTFUN2:2;
(g2 | m) /. n2 in rng (g2 | m)
by A234, PARTFUN2:2;
then A241:
(rng (g2 | m)) /\ (rng L) <> {}
by A240, XBOOLE_0:def 4;
A242:
i1 in dom G1
by A96, A236, ZFMISC_1:87;
the
Element of
(rng h2) /\ (rng (g2 | m)) = G1 * (
(ma + n1),
k2)
by A133, A230, A231;
then
i1 = ma + n1
by A235, A236, A237, A233, GOBOARD1:5;
then
n1 <= 0
by A41, A242, A241, XREAL_1:29;
hence
contradiction
by A232;
verum
end; then (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) =
(((rng h1) \/ (rng f)) /\ (rng (g2 | m))) \/ {}
by A196, XBOOLE_1:23
.=
{} \/ ((rng f) /\ (rng (g2 | m)))
by A112, XBOOLE_1:23
.=
(rng f) /\ (rng (g2 | m))
;
then A243:
(rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) c= (rng g1) /\ (rng g2)
by A18, A178, XBOOLE_1:27;
A244:
len (DelCol (G1,1)) = len G1
by MATRIX_0:def 13;
then A245:
dom (DelCol (G1,1)) =
Seg (len G1)
by FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
A246:
now for n being Nat st n in dom f & n + 1 in dom f holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & f /. n = G1 * (i1,i2) & f /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1let n be
Nat;
( n in dom f & n + 1 in dom f implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & f /. n = G1 * (i1,i2) & f /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A247:
n in dom f
and A248:
n + 1
in dom f
;
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & f /. n = G1 * (i1,i2) & f /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
f /. n = (g1 | mi1) /. (w + n)
by A155, A157, A247;
then A249:
f /. n = g1 /. (w + n)
by A170, A157, A247;
f /. (n + 1) = (g1 | mi1) /. (w + (n + 1))
by A155, A157, A248;
then A250:
(
(w + n) + 1
in dom g1 &
f /. (n + 1) = g1 /. ((w + n) + 1) )
by A170, A157, A248;
let i1,
i2,
j1,
j2 be
Nat;
( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & f /. n = G1 * (i1,i2) & f /. (n + 1) = G1 * (j1,j2) implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )assume A251:
(
[i1,i2] in Indices G1 &
[j1,j2] in Indices G1 &
f /. n = G1 * (
i1,
i2) &
f /. (n + 1) = G1 * (
j1,
j2) )
;
|.(i1 - j1).| + |.(i2 - j2).| = 1
w + n in dom g1
by A170, A157, A247;
hence
|.(i1 - j1).| + |.(i2 - j2).| = 1
by A6, A249, A250, A251, GOBOARD1:def 9;
verum end; set hf =
h1 ^ f;
A252:
len ((h1 ^ f) ^ h2) =
(len (h1 ^ f)) + (len h2)
by FINSEQ_1:22
.=
((len h1) + (len f)) + (len h2)
by FINSEQ_1:22
;
A253:
now for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ f) /. (len (h1 ^ f)) = G1 * (i1,i2) & h2 /. 1 = G1 * (j1,j2) & len (h1 ^ f) in dom (h1 ^ f) & 1 in dom h2 holds
|.(i1 - j1).| + |.(i2 - j2).| = 1let i1,
i2,
j1,
j2 be
Nat;
( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ f) /. (len (h1 ^ f)) = G1 * (i1,i2) & h2 /. 1 = G1 * (j1,j2) & len (h1 ^ f) in dom (h1 ^ f) & 1 in dom h2 implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A254:
[i1,i2] in Indices G1
and A255:
[j1,j2] in Indices G1
and A256:
(h1 ^ f) /. (len (h1 ^ f)) = G1 * (
i1,
i2)
and A257:
h2 /. 1
= G1 * (
j1,
j2)
and
len (h1 ^ f) in dom (h1 ^ f)
and A258:
1
in dom h2
;
|.(i1 - j1).| + |.(i2 - j2).| = 1
ma + 1
in dom G1
by A135, A258;
then A259:
[(ma + 1),k2] in Indices G1
by A134, A96, ZFMISC_1:87;
A260:
[ma,k2] in Indices G1
by A41, A134, A96, ZFMISC_1:87;
A261:
Lma /. k2 = Lma . k2
by A131, PARTFUN1:def 6;
A262:
len f in dom f
by A155, A157, A158, FINSEQ_1:1;
(h1 ^ f) /. (len (h1 ^ f)) =
(h1 ^ f) /. ((len h1) + (len f))
by FINSEQ_1:22
.=
f /. (len f)
by A262, FINSEQ_4:69
.=
(g1 | mi1) /. (w + l)
by A155, A157, A262
.=
g1 /. mi1
by A170, A155, A157, A262
.=
G1 * (
ma,
k2)
by A132, A134, A261, MATRIX_0:def 7
;
then A263:
(
i1 = ma &
i2 = k2 )
by A254, A256, A260, GOBOARD1:5;
h2 /. 1
= G1 * (
(ma + 1),
k2)
by A133, A258;
then
(
j1 = ma + 1 &
j2 = k2 )
by A255, A257, A259, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| =
|.(ma - (ma + 1)).| + 0
by A263, ABSVALUE:2
.=
|.(- ((ma + 1) - ma)).|
.=
|.1.|
by COMPLEX1:52
.=
1
by ABSVALUE:def 1
;
verum end; now for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. (len h1) = G1 * (i1,i2) & f /. 1 = G1 * (j1,j2) & len h1 in dom h1 & 1 in dom f holds
|.(i1 - j1).| + |.(i2 - j2).| = 1A264:
[mi,k1] in Indices G1
by A39, A51, A96, ZFMISC_1:87;
A265:
Lmi /. k1 = Lmi . k1
by A49, PARTFUN1:def 6;
let i1,
i2,
j1,
j2 be
Nat;
( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. (len h1) = G1 * (i1,i2) & f /. 1 = G1 * (j1,j2) & len h1 in dom h1 & 1 in dom f implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A266:
[i1,i2] in Indices G1
and A267:
[j1,j2] in Indices G1
and A268:
h1 /. (len h1) = G1 * (
i1,
i2)
and A269:
f /. 1
= G1 * (
j1,
j2)
and A270:
len h1 in dom h1
and A271:
1
in dom f
;
|.(i1 - j1).| + |.(i2 - j2).| = 1
l1 in dom G1
by A74, A97, A270;
then A272:
[l1,k1] in Indices G1
by A51, A96, ZFMISC_1:87;
A273:
w + 1
= ma1
;
then
f /. 1
= (g1 | mi1) /. ma1
by A155, A157, A271;
then f /. 1 =
g1 /. ma1
by A170, A157, A271, A273
.=
G1 * (
mi,
k1)
by A50, A51, A265, MATRIX_0:def 7
;
then A274:
(
j1 = mi &
j2 = k1 )
by A267, A269, A264, GOBOARD1:5;
h1 /. (len h1) = G1 * (
l1,
k1)
by A74, A270;
then
(
i1 = l1 &
i2 = k1 )
by A266, A268, A272, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| =
|.((mi - 1) - mi).| + 0
by A274, ABSVALUE:2
.=
|.(- 1).|
.=
|.1.|
by COMPLEX1:52
.=
1
by ABSVALUE:def 1
;
verum end; then
for
n being
Nat st
n in dom (h1 ^ f) &
n + 1
in dom (h1 ^ f) holds
for
i1,
i2,
j1,
j2 being
Nat st
[i1,i2] in Indices G1 &
[j1,j2] in Indices G1 &
(h1 ^ f) /. n = G1 * (
i1,
i2) &
(h1 ^ f) /. (n + 1) = G1 * (
j1,
j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
by A102, A246, GOBOARD1:24;
then A275:
for
n being
Nat st
n in dom ((h1 ^ f) ^ h2) &
n + 1
in dom ((h1 ^ f) ^ h2) holds
for
m,
k,
i,
j being
Nat st
[m,k] in Indices G1 &
[i,j] in Indices G1 &
((h1 ^ f) ^ h2) /. n = G1 * (
m,
k) &
((h1 ^ f) ^ h2) /. (n + 1) = G1 * (
i,
j) holds
|.(m - i).| + |.(k - j).| = 1
by A141, A253, GOBOARD1:24;
now for n being Nat st n in dom h1 holds
ex i, k1 being Nat st
( [i,k1] in Indices G1 & h1 /. n = G1 * (i,k1) )let n be
Nat;
( n in dom h1 implies ex i, k1 being Nat st
( [i,k1] in Indices G1 & h1 /. n = G1 * (i,k1) ) )assume A276:
n in dom h1
;
ex i, k1 being Nat st
( [i,k1] in Indices G1 & h1 /. n = G1 * (i,k1) )reconsider k1 =
k1 as
Nat ;
take i =
n;
ex k1 being Nat st
( [i,k1] in Indices G1 & h1 /. n = G1 * (i,k1) )take k1 =
k1;
( [i,k1] in Indices G1 & h1 /. n = G1 * (i,k1) )
n in dom G1
by A97, A276;
hence
(
[i,k1] in Indices G1 &
h1 /. n = G1 * (
i,
k1) )
by A74, A51, A96, A276, ZFMISC_1:87;
verum end; then
for
n being
Nat st
n in dom (h1 ^ f) holds
ex
i,
j being
Nat st
(
[i,j] in Indices G1 &
(h1 ^ f) /. n = G1 * (
i,
j) )
by A174, GOBOARD1:23;
then
for
n being
Nat st
n in dom ((h1 ^ f) ^ h2) holds
ex
i,
j being
Nat st
(
[i,j] in Indices G1 &
((h1 ^ f) ^ h2) /. n = G1 * (
i,
j) )
by A139, GOBOARD1:23;
then A277:
(h1 ^ f) ^ h2 is_sequence_on G1
by A275, GOBOARD1:def 9;
A278:
Seg (len ((h1 ^ f) ^ h2)) = dom ((h1 ^ f) ^ h2)
by FINSEQ_1:def 3;
then A279:
len ((h1 ^ f) ^ h2) in dom ((h1 ^ f) ^ h2)
by A252, A195, FINSEQ_1:1;
A280:
1
in dom ((h1 ^ f) ^ h2)
by A252, A195, A278, FINSEQ_1:1;
thus
(rng g1) /\ (rng g2) <> {}
verumproof
per cases
( (rng f) /\ (rng (Col (G1,1))) = {} or (rng f) /\ (rng (Col (G1,1))) <> {} )
;
suppose A281:
(rng f) /\ (rng (Col (G1,1))) = {}
;
(rng g1) /\ (rng g2) <> {} set D =
DelCol (
G1,1);
A282:
1
in Seg (width G1)
by A152, FINSEQ_1:1;
A283:
DelCol (
G1,1) is
V6()
by A152, A282, MATRIX_0:65;
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,1))) = {}
by A31, A197, A281;
then A284:
rng ((h1 ^ f) ^ h2) misses rng (Col (G1,1))
by XBOOLE_0:def 7;
then A285:
(
(h1 ^ f) ^ h2 is_sequence_on DelCol (
G1,1) &
((h1 ^ f) ^ h2) /. 1
in rng (Line ((DelCol (G1,1)),1)) )
by A31, A26, A277, A159, A152, A280, GOBOARD1:25, MATRIX_0:75;
A286:
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line ((DelCol (G1,1)),(len (DelCol (G1,1)))))
by A31, A27, A183, A152, A244, A279, A284, MATRIX_0:75;
defpred S7[
Nat]
means ( $1
in dom (g2 | m) &
(g2 | m) /. $1
in rng (Col (G1,1)) );
A287:
ex
m being
Nat st
S7[
m]
A288:
for
m being
Nat st
S7[
m] holds
m <= len (g2 | m)
by FINSEQ_3:25;
consider m being
Nat such that A289:
(
S7[
m] & ( for
k being
Nat st
S7[
k] holds
k <= m ) )
from NAT_1:sch 6(A288, A287);
reconsider m =
m as
Nat ;
reconsider p =
(g2 | m) /. m as
Point of
(TOP-REAL 2) ;
then reconsider ll =
(len (g2 | m)) - m as
Element of
NAT by INT_1:5;
deffunc H3(
Nat)
-> Element of the
U1 of
(TOP-REAL 2) =
(g2 | m) /. (m + $1);
consider t being
FinSequence of
(TOP-REAL 2) such that A292:
(
len t = ll & ( for
n being
Nat st
n in dom t holds
t /. n = H3(
n) ) )
from FINSEQ_4:sch 2();
A293:
dom t = Seg ll
by A292, FINSEQ_1:def 3;
A294:
rng t c= rng (g2 | m)
A299:
for
n being
Nat st
n in dom t holds
m + n in dom (g2 | m)
A303:
Seg (len t) = dom t
by FINSEQ_1:def 3;
reconsider t =
t as
FinSequence of
(TOP-REAL 2) ;
A304:
width (DelCol (G1,1)) = k
by A3, A31, MATRIX_0:63;
A305:
Indices (DelCol (G1,1)) = [:(dom (DelCol (G1,1))),(Seg (width (DelCol (G1,1)))):]
by MATRIX_0:def 4;
A306:
now for n being Nat st n in dom t holds
ex i1, l being Nat st
( [i1,l] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,l) )let n be
Nat;
( n in dom t implies ex i1, l being Nat st
( [i1,l] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,l) ) )assume A307:
n in dom t
;
ex i1, l being Nat st
( [i1,l] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,l) )then
m + n in dom (g2 | m)
by A299;
then consider i1,
i2 being
Nat such that A308:
[i1,i2] in Indices G1
and A309:
(g2 | m) /. (m + n) = G1 * (
i1,
i2)
by A15, GOBOARD1:def 9;
A310:
i2 in Seg (width G1)
by A96, A308, ZFMISC_1:87;
then A311:
1
<= i2
by FINSEQ_1:1;
then reconsider l =
i2 - 1 as
Element of
NAT by INT_1:5;
reconsider Ci2 =
Col (
G1,
i2) as
FinSequence of
(TOP-REAL 2) ;
A312:
i1 in dom G1
by A96, A308, ZFMISC_1:87;
len Ci2 = len G1
by MATRIX_0:def 8;
then A313:
dom Ci2 =
Seg (len G1)
by FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
then
Ci2 /. i1 = Ci2 . i1
by A312, PARTFUN1:def 6;
then
Ci2 /. i1 = G1 * (
i1,
i2)
by A312, MATRIX_0:def 8;
then A314:
(g2 | m) /. (m + n) in rng (Col (G1,i2))
by A309, A312, A313, PARTFUN2:2;
then
1
< i2
by A311, XXREAL_0:1;
then
1
+ 1
<= i2
by NAT_1:13;
then A316:
1
<= l
by XREAL_1:19;
reconsider i1 =
i1,
l =
l as
Nat ;
take i1 =
i1;
ex l being Nat st
( [i1,l] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,l) )take l =
l;
( [i1,l] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,l) )A317:
t /. n = (g2 | m) /. (m + n)
by A292, A307;
i2 <= width G1
by A310, FINSEQ_1:1;
then A318:
l <= width (DelCol (G1,1))
by A3, A304, XREAL_1:20;
then
l in Seg (width (DelCol (G1,1)))
by A316, FINSEQ_1:1;
hence
[i1,l] in Indices (DelCol (G1,1))
by A245, A305, A312, ZFMISC_1:87;
t /. n = (DelCol (G1,1)) * (i1,l)
l + 1
= i2
;
hence
t /. n = (DelCol (G1,1)) * (
i1,
l)
by A3, A31, A304, A309, A312, A317, A316, A318, MATRIX_0:70;
verum end;
0 < width (DelCol (G1,1))
by A283, MATRIX_0:def 10, NAT_1:3;
then A319:
0 + 1
<= width (DelCol (G1,1))
by NAT_1:13;
then A320:
(
Col (
(DelCol (G1,1)),1)
= Col (
G1,
(1 + 1)) & 1
+ 1
in Seg (width G1) )
by A3, A31, A304, MATRIX_0:68;
m + 1
<= len (g2 | m)
by A290, NAT_1:13;
then A321:
1
<= len t
by A292, XREAL_1:19;
then
t /. 1
= (g2 | m) /. (m + 1)
by A292, A303, FINSEQ_1:1;
then A322:
t /. 1
in rng (Col ((DelCol (G1,1)),1))
by A32, A15, A28, A31, A289, A320, GOBOARD1:32;
now for n being Nat st n in dom t & n + 1 in dom t holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices (DelCol (G1,1)) & [j1,j2] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,i2) & t /. (n + 1) = (DelCol (G1,1)) * (j1,j2) holds
1 = |.(i1 - j1).| + |.(i2 - j2).|let n be
Nat;
( n in dom t & n + 1 in dom t implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices (DelCol (G1,1)) & [j1,j2] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,i2) & t /. (n + 1) = (DelCol (G1,1)) * (j1,j2) holds
1 = |.(i1 - j1).| + |.(i2 - j2).| )assume that A323:
n in dom t
and A324:
n + 1
in dom t
;
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices (DelCol (G1,1)) & [j1,j2] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,i2) & t /. (n + 1) = (DelCol (G1,1)) * (j1,j2) holds
1 = |.(i1 - j1).| + |.(i2 - j2).|let i1,
i2,
j1,
j2 be
Nat;
( [i1,i2] in Indices (DelCol (G1,1)) & [j1,j2] in Indices (DelCol (G1,1)) & t /. n = (DelCol (G1,1)) * (i1,i2) & t /. (n + 1) = (DelCol (G1,1)) * (j1,j2) implies 1 = |.(i1 - j1).| + |.(i2 - j2).| )assume that A325:
[i1,i2] in Indices (DelCol (G1,1))
and A326:
[j1,j2] in Indices (DelCol (G1,1))
and A327:
t /. n = (DelCol (G1,1)) * (
i1,
i2)
and A328:
t /. (n + 1) = (DelCol (G1,1)) * (
j1,
j2)
;
1 = |.(i1 - j1).| + |.(i2 - j2).|A329:
i1 in dom (DelCol (G1,1))
by A305, A325, ZFMISC_1:87;
i2 in Seg k
by A304, A305, A325, ZFMISC_1:87;
then A330:
( 1
<= i2 &
i2 <= k )
by FINSEQ_1:1;
then
i2 + 1
in Seg (width G1)
by A3, A31, A245, A329, MATRIX_0:70;
then A331:
[i1,(i2 + 1)] in Indices G1
by A96, A245, A329, ZFMISC_1:87;
t /. n = (g2 | m) /. (m + n)
by A292, A323;
then A332:
(g2 | m) /. (m + n) = G1 * (
i1,
(i2 + 1))
by A3, A31, A245, A327, A329, A330, MATRIX_0:70;
m + (n + 1) = (m + n) + 1
;
then A333:
(m + n) + 1
in dom (g2 | m)
by A299, A324;
A334:
j1 in dom (DelCol (G1,1))
by A305, A326, ZFMISC_1:87;
j2 in Seg k
by A304, A305, A326, ZFMISC_1:87;
then A335:
( 1
<= j2 &
j2 <= k )
by FINSEQ_1:1;
then
j2 + 1
in Seg (width G1)
by A3, A31, A245, A329, MATRIX_0:70;
then A336:
[j1,(j2 + 1)] in Indices G1
by A96, A245, A334, ZFMISC_1:87;
t /. (n + 1) = (g2 | m) /. (m + (n + 1))
by A292, A324;
then A337:
(g2 | m) /. ((m + n) + 1) = G1 * (
j1,
(j2 + 1))
by A3, A31, A245, A328, A334, A335, MATRIX_0:70;
m + n in dom (g2 | m)
by A299, A323;
hence 1 =
|.(i1 - j1).| + |.((i2 + 1) - (j2 + 1)).|
by A15, A332, A337, A331, A336, A333, GOBOARD1:def 9
.=
|.(i1 - j1).| + |.(i2 - j2).|
;
verum end; then A338:
t is_sequence_on DelCol (
G1,1)
by A306, GOBOARD1:def 9;
set x = the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng t);
A339:
(rng ((h1 ^ f) ^ h2)) /\ (rng t) c= (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m))
by A294, XBOOLE_1:26;
len t in Seg ll
by A292, A321, FINSEQ_1:1;
then t /. (len t) =
(g2 | m) /. (m + ll)
by A292, A303
.=
(g2 | m) /. (len (g2 | m))
;
then
t /. (len t) in rng (Col ((DelCol (G1,1)),(width (DelCol (G1,1)))))
by A3, A28, A31, A304, A319, MATRIX_0:68;
then
(rng ((h1 ^ f) ^ h2)) /\ (rng t) <> {}
by A2, A92, A252, A195, A304, A321, A322, A338, A285, A286, A283;
then
the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng t) in (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m))
by A339;
hence
(rng g1) /\ (rng g2) <> {}
by A243;
verum end; suppose A340:
(rng f) /\ (rng (Col (G1,1))) <> {}
;
(rng g1) /\ (rng g2) <> {} set D =
DelCol (
G1,
(width G1));
A341:
DelCol (
G1,
(width G1)) is
V6()
by A93, A94, MATRIX_0:65;
A342:
0 + 1
< k + 1
by A92, XREAL_1:6;
now (rng g1) /\ (rng g2) <> {} per cases
( (rng f) /\ (rng (Col (G1,(width G1)))) = {} or (rng f) /\ (rng (Col (G1,(width G1)))) <> {} )
;
suppose
(rng f) /\ (rng (Col (G1,(width G1)))) = {}
;
(rng g1) /\ (rng g2) <> {} then
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,(width G1)))) = {}
by A73, A197;
then A343:
rng ((h1 ^ f) ^ h2) misses rng (Col (G1,(width G1)))
by XBOOLE_0:def 7;
then A344:
(h1 ^ f) ^ h2 is_sequence_on DelCol (
G1,
(width G1))
by A73, A277, A152, GOBOARD1:25;
consider t being
FinSequence of
(TOP-REAL 2) such that A345:
(
t /. 1
in rng (Col ((DelCol (G1,(width G1))),1)) &
t /. (len t) in rng (Col ((DelCol (G1,(width G1))),(width (DelCol (G1,(width G1)))))) & 1
<= len t &
t is_sequence_on DelCol (
G1,
(width G1)) )
and A346:
rng t c= rng (g2 | m)
by A3, A32, A15, A14, A28, A342, GOBOARD1:35;
set x = the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng t);
A347:
(rng ((h1 ^ f) ^ h2)) /\ (rng t) c= (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m))
by A346, XBOOLE_1:26;
A348:
width (DelCol (G1,(width G1))) = k
by A3, A73, MATRIX_0:63;
(
((h1 ^ f) ^ h2) /. 1
in rng (Line ((DelCol (G1,(width G1))),1)) &
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line ((DelCol (G1,(width G1))),(len (DelCol (G1,(width G1)))))) )
by A73, A26, A27, A159, A183, A152, A153, A280, A279, A343, MATRIX_0:75;
then
(rng ((h1 ^ f) ^ h2)) /\ (rng t) <> {}
by A2, A92, A252, A195, A345, A348, A344, A341;
then
the
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng t) in (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m))
by A347;
hence
(rng g1) /\ (rng g2) <> {}
by A243;
verum end; suppose A349:
(rng f) /\ (rng (Col (G1,(width G1)))) <> {}
;
(rng g1) /\ (rng g2) <> {} A350:
f is_sequence_on G1
by A174, A246, GOBOARD1:def 9;
then consider t being
FinSequence of
(TOP-REAL 2) such that A351:
rng t c= rng f
and A352:
(
t /. 1
in rng (Col (G1,1)) &
t /. (len t) in rng (Col (G1,(width G1))) & 1
<= len t &
t is_sequence_on G1 )
by A340, A349, GOBOARD1:36;
consider tt being
FinSequence of
(TOP-REAL 2) such that A353:
(
tt /. 1
in rng (Col ((DelCol (G1,(width G1))),1)) &
tt /. (len tt) in rng (Col ((DelCol (G1,(width G1))),(width (DelCol (G1,(width G1)))))) & 1
<= len tt &
tt is_sequence_on DelCol (
G1,
(width G1)) )
and A354:
rng tt c= rng t
by A3, A342, A352, GOBOARD1:35;
A355:
(
Seg (len Lma) = dom Lma &
len Lma = width G1 )
by FINSEQ_1:def 3, MATRIX_0:def 7;
reconsider lg =
(len (g2 | m)) - 1 as
Element of
NAT by A32, INT_1:5;
defpred S7[
Nat]
means ( $1
in dom (g2 | m) &
(g2 | m) /. $1
in rng (Line (G1,mi)) );
defpred S8[
Nat]
means ( $1
in dom (g2 | m) &
(g2 | m) /. $1
in rng (Line (G1,ma)) );
A356:
lg <= len (g2 | m)
by XREAL_1:43;
A357:
now ex n being Nat st S7[n]end; consider pf being
Nat such that A359:
(
S7[
pf] & ( for
n being
Nat st
S7[
n] holds
pf <= n ) )
from NAT_1:sch 5(A357);
defpred S9[
Nat]
means ( $1
in dom f implies for
m being
Nat st
m in dom G1 &
f /. $1
in rng (Line (G1,m)) holds
mi <= m );
reconsider C =
Col (
G1,
(width G1)),
Li =
Line (
G1,
mi),
La =
Line (
G1,
ma) as
FinSequence of
(TOP-REAL 2) ;
A360:
lg + 1
= len (g2 | m)
;
A361:
now ex n being Nat st S8[n]end; consider pl being
Nat such that A363:
(
S8[
pl] & ( for
n being
Nat st
S8[
n] holds
pl <= n ) )
from NAT_1:sch 5(A361);
reconsider pf =
pf,
pl =
pl as
Nat ;
A364:
1
<= pf
by A359, FINSEQ_3:25;
consider K2 being
Element of
NAT such that A365:
K2 in dom Lma
and A366:
(g2 | m) /. pl = Lma /. K2
by A363, PARTFUN2:2;
reconsider CK2 =
Col (
G1,
K2) as
FinSequence of
(TOP-REAL 2) ;
consider K1 being
Element of
NAT such that A367:
K1 in dom Li
and A368:
(g2 | m) /. pf = Li /. K1
by A359, PARTFUN2:2;
reconsider CK1 =
Col (
G1,
K1) as
FinSequence of
(TOP-REAL 2) ;
deffunc H3(
Nat)
-> Element of the
U1 of
(TOP-REAL 2) =
G1 * ($1,
K1);
consider h1 being
FinSequence of
(TOP-REAL 2) such that A369:
(
len h1 = l1 & ( for
n being
Nat st
n in dom h1 holds
h1 /. n = H3(
n) ) )
from FINSEQ_4:sch 2();
A370:
for
k being
Nat st
S9[
k] holds
S9[
k + 1]
proof
let k be
Nat;
( S9[k] implies S9[k + 1] )
assume A371:
S9[
k]
;
S9[k + 1]
assume A372:
k + 1
in dom f
;
for m being Nat st m in dom G1 & f /. (k + 1) in rng (Line (G1,m)) holds
mi <= m
let m be
Nat;
( m in dom G1 & f /. (k + 1) in rng (Line (G1,m)) implies mi <= m )
assume A373:
(
m in dom G1 &
f /. (k + 1) in rng (Line (G1,m)) )
;
mi <= m
now mi <= mper cases
( k = 0 or k <> 0 )
;
suppose
k <> 0
;
mi <= mthen
0 < k
;
then A375:
0 + 1
<= k
by NAT_1:13;
k + 1
<= len f
by A372, FINSEQ_3:25;
then A376:
k <= len f
by NAT_1:13;
then A377:
k in dom f
by A375, FINSEQ_3:25;
then consider i1,
i2 being
Nat such that A378:
[i1,i2] in Indices G1
and A379:
f /. k = G1 * (
i1,
i2)
by A174;
A380:
i2 in Seg (width G1)
by A96, A378, ZFMISC_1:87;
consider j1,
j2 being
Nat such that A381:
[j1,j2] in Indices G1
and A382:
f /. (k + 1) = G1 * (
j1,
j2)
by A174, A372;
reconsider Lj1 =
Line (
G1,
j1) as
FinSequence of
(TOP-REAL 2) ;
A383:
j2 in Seg (width G1)
by A96, A381, ZFMISC_1:87;
A384:
(
Seg (len Lj1) = dom Lj1 &
len Lj1 = width G1 )
by FINSEQ_1:def 3, MATRIX_0:def 7;
then
Lj1 /. j2 = Lj1 . j2
by A383, PARTFUN1:def 6;
then
f /. (k + 1) = Lj1 /. j2
by A382, A383, MATRIX_0:def 7;
then A385:
f /. (k + 1) in rng Lj1
by A383, A384, PARTFUN2:2;
A386:
j1 in dom G1
by A96, A381, ZFMISC_1:87;
reconsider Li1 =
Line (
G1,
i1) as
FinSequence of
(TOP-REAL 2) ;
A387:
i1 in dom G1
by A96, A378, ZFMISC_1:87;
A388:
(
Seg (len Li1) = dom Li1 &
len Li1 = width G1 )
by FINSEQ_1:def 3, MATRIX_0:def 7;
then A389:
Li1 /. i2 = Li1 . i2
by A380, PARTFUN1:def 6;
then
f /. k = Li1 /. i2
by A379, A380, MATRIX_0:def 7;
then A390:
f /. k in rng Li1
by A380, A388, PARTFUN2:2;
then A391:
mi <= i1
by A371, A375, A376, A387, FINSEQ_3:25;
now mi <= mper cases
( mi = i1 or mi < i1 )
by A391, XXREAL_0:1;
suppose A392:
mi = i1
;
mi <= mg1 /. (w + k) =
(g1 | mi1) /. (w + k)
by A170, A157, A377
.=
f /. k
by A155, A157, A377
.=
Li1 /. i2
by A379, A380, A389, MATRIX_0:def 7
;
then
g1 /. (w + k) in rng (Line (G1,mi))
by A380, A388, A392, PARTFUN2:2;
then A393:
w + k <= ma1
by A46, A170, A157, A377;
w + 1
<= w + k
by A375, XREAL_1:7;
then
w + k = ma1
by A393, XXREAL_0:1;
then A394:
ma1 + 1
= w + (k + 1)
;
mi + 1
<= ma
by A128, NAT_1:13;
then A395:
mi + 1
<= len G1
by A48, XXREAL_0:2;
1
<= mi + 1
by A42, NAT_1:13;
then A396:
mi + 1
in dom G1
by A395, FINSEQ_3:25;
(
f /. (k + 1) = (g1 | mi1) /. (w + (k + 1)) &
(g1 | mi1) /. (w + (k + 1)) = g1 /. (w + (k + 1)) )
by A170, A155, A157, A372;
then
f /. (k + 1) in rng (Line (G1,(mi + 1)))
by A4, A6, A9, A39, A46, A394, A396, GOBOARD1:28;
then
m = mi + 1
by A373, A396, GOBOARD1:3;
hence
mi <= m
by NAT_1:11;
verum end; end; end; hence
mi <= m
;
verum end; end; end;
hence
mi <= m
;
verum
end; A400:
(
Seg (len Li) = dom Li &
len Li = width G1 )
by FINSEQ_1:def 3, MATRIX_0:def 7;
A406:
now for n being Nat st n in dom h1 holds
ex i, K1 being Nat st
( [i,K1] in Indices G1 & h1 /. n = G1 * (i,K1) )let n be
Nat;
( n in dom h1 implies ex i, K1 being Nat st
( [i,K1] in Indices G1 & h1 /. n = G1 * (i,K1) ) )assume A407:
n in dom h1
;
ex i, K1 being Nat st
( [i,K1] in Indices G1 & h1 /. n = G1 * (i,K1) )reconsider i =
n,
K1 =
K1 as
Nat ;
take i =
i;
ex K1 being Nat st
( [i,K1] in Indices G1 & h1 /. n = G1 * (i,K1) )take K1 =
K1;
( [i,K1] in Indices G1 & h1 /. n = G1 * (i,K1) )
n in dom G1
by A401, A407;
hence
(
[i,K1] in Indices G1 &
h1 /. n = G1 * (
i,
K1) )
by A96, A367, A400, A369, A407, ZFMISC_1:87;
verum end; A408:
now for n being Nat st n in dom h1 & n + 1 in dom h1 holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. n = G1 * (i1,i2) & h1 /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1let n be
Nat;
( n in dom h1 & n + 1 in dom h1 implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. n = G1 * (i1,i2) & h1 /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A409:
n in dom h1
and A410:
n + 1
in dom h1
;
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. n = G1 * (i1,i2) & h1 /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
n + 1
in dom G1
by A401, A410;
then A411:
[(n + 1),K1] in Indices G1
by A96, A367, A400, ZFMISC_1:87;
let i1,
i2,
j1,
j2 be
Nat;
( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. n = G1 * (i1,i2) & h1 /. (n + 1) = G1 * (j1,j2) implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A412:
[i1,i2] in Indices G1
and A413:
[j1,j2] in Indices G1
and A414:
h1 /. n = G1 * (
i1,
i2)
and A415:
h1 /. (n + 1) = G1 * (
j1,
j2)
;
|.(i1 - j1).| + |.(i2 - j2).| = 1
h1 /. (n + 1) = G1 * (
(n + 1),
K1)
by A369, A410;
then A416:
(
j1 = n + 1 &
j2 = K1 )
by A411, A413, A415, GOBOARD1:5;
n in dom G1
by A401, A409;
then A417:
[n,K1] in Indices G1
by A96, A367, A400, ZFMISC_1:87;
h1 /. n = G1 * (
n,
K1)
by A369, A409;
then
(
i1 = n &
i2 = K1 )
by A417, A412, A414, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| =
|.((n - n) + (- 1)).| + 0
by A416, ABSVALUE:2
.=
|.1.|
by COMPLEX1:52
.=
1
by ABSVALUE:def 1
;
verum end; A418:
pf <= len (g2 | m)
by A359, FINSEQ_3:25;
A419:
Lma /. K2 = Lma . K2
by A365, PARTFUN1:def 6;
then A420:
(g2 | m) /. pl = G1 * (
ma,
K2)
by A365, A366, A355, MATRIX_0:def 7;
deffunc H4(
Nat)
-> Element of the
U1 of
(TOP-REAL 2) =
G1 * (
(ma + $1),
K2);
consider h2 being
FinSequence of
(TOP-REAL 2) such that A421:
(
len h2 = l2 & ( for
n being
Nat st
n in dom h2 holds
h2 /. n = H4(
n) ) )
from FINSEQ_4:sch 2();
A422:
S9[
0 ]
by FINSEQ_3:25;
A423:
for
n being
Nat holds
S9[
n]
from NAT_1:sch 2(A422, A370);
A424:
(rng h1) /\ (rng tt) = {}
proof
set x = the
Element of
(rng h1) /\ (rng tt);
assume A425:
not
(rng h1) /\ (rng tt) = {}
;
contradiction
then
the
Element of
(rng h1) /\ (rng tt) in rng h1
by XBOOLE_0:def 4;
then consider i2 being
Element of
NAT such that A426:
i2 in dom h1
and A427:
h1 /. i2 = the
Element of
(rng h1) /\ (rng tt)
by PARTFUN2:2;
Seg (len h1) = dom h1
by FINSEQ_1:def 3;
then A428:
(
l1 < mi &
i2 <= l1 )
by A369, A426, FINSEQ_1:1, XREAL_1:44;
i2 in dom G1
by A401, A426;
then A429:
[i2,K1] in Indices G1
by A96, A367, A400, ZFMISC_1:87;
the
Element of
(rng h1) /\ (rng tt) in rng tt
by A425, XBOOLE_0:def 4;
then
the
Element of
(rng h1) /\ (rng tt) in rng t
by A354;
then consider i1 being
Element of
NAT such that A430:
i1 in dom f
and A431:
f /. i1 = the
Element of
(rng h1) /\ (rng tt)
by A351, PARTFUN2:2;
consider n1,
n2 being
Nat such that A432:
[n1,n2] in Indices G1
and A433:
f /. i1 = G1 * (
n1,
n2)
by A174, A430;
reconsider Ln1 =
Line (
G1,
n1) as
FinSequence of
(TOP-REAL 2) ;
A434:
n2 in Seg (width G1)
by A96, A432, ZFMISC_1:87;
A435:
(
Seg (len Ln1) = dom Ln1 &
len Ln1 = width G1 )
by FINSEQ_1:def 3, MATRIX_0:def 7;
then
Ln1 /. n2 = Ln1 . n2
by A434, PARTFUN1:def 6;
then
f /. i1 = Ln1 /. n2
by A433, A434, MATRIX_0:def 7;
then A436:
f /. i1 in rng Ln1
by A434, A435, PARTFUN2:2;
n1 in dom G1
by A96, A432, ZFMISC_1:87;
then A437:
mi <= n1
by A423, A430, A436;
the
Element of
(rng h1) /\ (rng tt) = G1 * (
i2,
K1)
by A369, A426, A427;
then
i2 = n1
by A431, A432, A433, A429, GOBOARD1:5;
hence
contradiction
by A437, A428, XXREAL_0:2;
verum
end; defpred S10[
Nat]
means ( $1
in dom f implies for
m being
Nat st
m in dom G1 &
f /. $1
in rng (Line (G1,m)) holds
m <= ma );
A438:
for
k being
Nat st
S10[
k] holds
S10[
k + 1]
proof
let k be
Nat;
( S10[k] implies S10[k + 1] )
assume A439:
S10[
k]
;
S10[k + 1]
assume A440:
k + 1
in dom f
;
for m being Nat st m in dom G1 & f /. (k + 1) in rng (Line (G1,m)) holds
m <= ma
let m be
Nat;
( m in dom G1 & f /. (k + 1) in rng (Line (G1,m)) implies m <= ma )
assume A441:
(
m in dom G1 &
f /. (k + 1) in rng (Line (G1,m)) )
;
m <= ma
now m <= maper cases
( k = 0 or k <> 0 )
;
suppose A443:
k <> 0
;
m <= maA444:
k + 1
<= len f
by A177, A440, FINSEQ_1:1;
then A445:
k <= len f
by NAT_1:13;
consider j1,
j2 being
Nat such that A446:
[j1,j2] in Indices G1
and A447:
f /. (k + 1) = G1 * (
j1,
j2)
by A174, A440;
reconsider Lj1 =
Line (
G1,
j1) as
FinSequence of
(TOP-REAL 2) ;
A448:
j2 in Seg (width G1)
by A96, A446, ZFMISC_1:87;
A449:
(
Seg (len Lj1) = dom Lj1 &
len Lj1 = width G1 )
by FINSEQ_1:def 3, MATRIX_0:def 7;
then
Lj1 /. j2 = Lj1 . j2
by A448, PARTFUN1:def 6;
then
f /. (k + 1) = Lj1 /. j2
by A447, A448, MATRIX_0:def 7;
then A450:
f /. (k + 1) in rng Lj1
by A448, A449, PARTFUN2:2;
A451:
j1 in dom G1
by A96, A446, ZFMISC_1:87;
then A452:
j1 = m
by A441, A450, GOBOARD1:3;
0 < k
by A443;
then A453:
0 + 1
<= k
by NAT_1:13;
then A454:
k in dom f
by A445, FINSEQ_3:25;
then consider i1,
i2 being
Nat such that A455:
[i1,i2] in Indices G1
and A456:
f /. k = G1 * (
i1,
i2)
by A174;
reconsider Li1 =
Line (
G1,
i1) as
FinSequence of
(TOP-REAL 2) ;
A457:
i2 in Seg (width G1)
by A96, A455, ZFMISC_1:87;
A458:
(
Seg (len Li1) = dom Li1 &
len Li1 = width G1 )
by FINSEQ_1:def 3, MATRIX_0:def 7;
then
Li1 /. i2 = Li1 . i2
by A457, PARTFUN1:def 6;
then
f /. k = Li1 /. i2
by A456, A457, MATRIX_0:def 7;
then A459:
f /. k in rng Li1
by A457, A458, PARTFUN2:2;
A460:
i1 in dom G1
by A96, A455, ZFMISC_1:87;
then A461:
i1 <= ma
by A439, A453, A445, A459, FINSEQ_3:25;
now ( ( ma = i1 & contradiction ) or ( i1 < ma & m <= ma ) )per cases
( ma = i1 or i1 < ma )
by A461, XXREAL_0:1;
case A462:
ma = i1
;
contradictionA463:
w + 1
<= w + k
by A453, XREAL_1:7;
A464:
(
f /. k = (g1 | mi1) /. (w + k) &
(g1 | mi1) /. (w + k) = g1 /. (w + k) )
by A170, A155, A157, A454;
then
ma1 <> w + k
by A39, A41, A46, A95, A459, A462, GOBOARD1:3;
then
ma1 < w + k
by A463, XXREAL_0:1;
then A465:
mi1 <= w + k
by A130, A170, A157, A454, A459, A462, A464;
w + k <= mi1
by A155, A156, A445, XREAL_1:7;
then
w + k = mi1
by A465, XXREAL_0:1;
hence
contradiction
by A155, A444, NAT_1:13;
verum end; end; end; hence
m <= ma
;
verum end; end; end;
hence
m <= ma
;
verum
end; A468:
Seg (len h1) = dom h1
by FINSEQ_1:def 3;
A473:
now for n being Nat st n in dom h2 holds
ex m, K2 being Nat st
( [m,K2] in Indices G1 & h2 /. n = G1 * (m,K2) )let n be
Nat;
( n in dom h2 implies ex m, K2 being Nat st
( [m,K2] in Indices G1 & h2 /. n = G1 * (m,K2) ) )assume A474:
n in dom h2
;
ex m, K2 being Nat st
( [m,K2] in Indices G1 & h2 /. n = G1 * (m,K2) )reconsider m =
ma + n,
K2 =
K2 as
Nat ;
take m =
m;
ex K2 being Nat st
( [m,K2] in Indices G1 & h2 /. n = G1 * (m,K2) )take K2 =
K2;
( [m,K2] in Indices G1 & h2 /. n = G1 * (m,K2) )
ma + n in dom G1
by A469, A474;
hence
(
[m,K2] in Indices G1 &
h2 /. n = G1 * (
m,
K2) )
by A96, A365, A355, A421, A474, ZFMISC_1:87;
verum end; A475:
now for n being Nat st n in dom h2 & n + 1 in dom h2 holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h2 /. n = G1 * (i1,i2) & h2 /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1let n be
Nat;
( n in dom h2 & n + 1 in dom h2 implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h2 /. n = G1 * (i1,i2) & h2 /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A476:
n in dom h2
and A477:
n + 1
in dom h2
;
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h2 /. n = G1 * (i1,i2) & h2 /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
ma + (n + 1) in dom G1
by A469, A477;
then A478:
[((ma + n) + 1),K2] in Indices G1
by A96, A365, A355, ZFMISC_1:87;
let i1,
i2,
j1,
j2 be
Nat;
( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h2 /. n = G1 * (i1,i2) & h2 /. (n + 1) = G1 * (j1,j2) implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A479:
[i1,i2] in Indices G1
and A480:
[j1,j2] in Indices G1
and A481:
h2 /. n = G1 * (
i1,
i2)
and A482:
h2 /. (n + 1) = G1 * (
j1,
j2)
;
|.(i1 - j1).| + |.(i2 - j2).| = 1
h2 /. (n + 1) = G1 * (
(ma + (n + 1)),
K2)
by A421, A477;
then A483:
(
j1 = (ma + n) + 1 &
j2 = K2 )
by A478, A480, A482, GOBOARD1:5;
ma + n in dom G1
by A469, A476;
then A484:
[(ma + n),K2] in Indices G1
by A96, A365, A355, ZFMISC_1:87;
h2 /. n = G1 * (
(ma + n),
K2)
by A421, A476;
then
(
i1 = ma + n &
i2 = K2 )
by A484, A479, A481, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| =
|.(((ma + n) - (ma + n)) + (- 1)).| + 0
by A483, ABSVALUE:2
.=
|.1.|
by COMPLEX1:52
.=
1
by ABSVALUE:def 1
;
verum end; A485:
Seg (len h2) = dom h2
by FINSEQ_1:def 3;
A486:
pl <= len (g2 | m)
by A363, FINSEQ_3:25;
A487:
1
<= pl
by A363, FINSEQ_3:25;
A488:
pl <> pf
by A39, A41, A95, A359, A363, GOBOARD1:3;
then
1
<= (len (g2 | m)) - 1
by XREAL_1:19;
then A489:
lg in dom (g2 | m)
by A356, FINSEQ_3:25;
A490:
S10[
0 ]
by FINSEQ_3:25;
A491:
for
n being
Nat holds
S10[
n]
from NAT_1:sch 2(A490, A438);
A492:
(rng h2) /\ (rng tt) = {}
proof
set x = the
Element of
(rng h2) /\ (rng tt);
assume A493:
not
(rng h2) /\ (rng tt) = {}
;
contradiction
then
the
Element of
(rng h2) /\ (rng tt) in rng h2
by XBOOLE_0:def 4;
then consider i2 being
Element of
NAT such that A494:
i2 in dom h2
and A495:
h2 /. i2 = the
Element of
(rng h2) /\ (rng tt)
by PARTFUN2:2;
0 + 1
<= i2
by A494, FINSEQ_3:25;
then A496:
0 < i2
;
ma + i2 in dom G1
by A469, A494;
then A497:
[(ma + i2),K2] in Indices G1
by A96, A365, A355, ZFMISC_1:87;
the
Element of
(rng h2) /\ (rng tt) in rng tt
by A493, XBOOLE_0:def 4;
then
the
Element of
(rng h2) /\ (rng tt) in rng t
by A354;
then consider i1 being
Element of
NAT such that A498:
i1 in dom f
and A499:
f /. i1 = the
Element of
(rng h2) /\ (rng tt)
by A351, PARTFUN2:2;
consider n1,
n2 being
Nat such that A500:
[n1,n2] in Indices G1
and A501:
f /. i1 = G1 * (
n1,
n2)
by A174, A498;
reconsider Ln1 =
Line (
G1,
n1) as
FinSequence of
(TOP-REAL 2) ;
A502:
n2 in Seg (width G1)
by A96, A500, ZFMISC_1:87;
A503:
(
Seg (len Ln1) = dom Ln1 &
len Ln1 = width G1 )
by FINSEQ_1:def 3, MATRIX_0:def 7;
then
Ln1 /. n2 = Ln1 . n2
by A502, PARTFUN1:def 6;
then
f /. i1 = Ln1 /. n2
by A501, A502, MATRIX_0:def 7;
then A504:
f /. i1 in rng Ln1
by A502, A503, PARTFUN2:2;
A505:
n1 in dom G1
by A96, A500, ZFMISC_1:87;
the
Element of
(rng h2) /\ (rng tt) = G1 * (
(ma + i2),
K2)
by A421, A494, A495;
then
ma + i2 = n1
by A499, A500, A501, A497, GOBOARD1:5;
hence
contradiction
by A491, A498, A505, A504, A496, XREAL_1:29;
verum
end;
1
<= len (g2 | m)
by A13, GOBOARD1:22;
then A506:
len (g2 | m) in dom (g2 | m)
by FINSEQ_3:25;
A507:
dom (g2 | m) c= dom g2
by A23, A24, A16, A17, FINSEQ_1:5;
now not pl = len (g2 | m)consider i2 being
Element of
NAT such that A508:
i2 in dom C
and A509:
C /. i2 = (g2 | m) /. (len (g2 | m))
by A28, PARTFUN2:2;
A510:
dom C =
Seg (len C)
by FINSEQ_1:def 3
.=
Seg (len G1)
by MATRIX_0:def 8
.=
dom G1
by FINSEQ_1:def 3
;
then A511:
[i2,(width G1)] in Indices G1
by A73, A96, A508, ZFMISC_1:87;
C /. i2 = C . i2
by A508, PARTFUN1:def 6;
then A512:
(g2 | m) /. (len (g2 | m)) = G1 * (
i2,
(width G1))
by A508, A509, A510, MATRIX_0:def 8;
assume A513:
pl = len (g2 | m)
;
contradictionconsider n1,
n2 being
Nat such that A514:
[n1,n2] in Indices G1
and A515:
(g2 | m) /. lg = G1 * (
n1,
n2)
by A15, A489, GOBOARD1:def 9;
A516:
n1 in dom G1
by A96, A514, ZFMISC_1:87;
A517:
n2 in Seg (width G1)
by A96, A514, ZFMISC_1:87;
[ma,K2] in Indices G1
by A41, A96, A365, A355, ZFMISC_1:87;
then
i2 = ma
by A420, A513, A512, A511, GOBOARD1:5;
then A518:
|.(n1 - ma).| + |.(n2 - (width G1)).| = 1
by A15, A489, A506, A360, A512, A511, A514, A515, GOBOARD1:def 9;
now contradictionper cases
( ( |.(n1 - ma).| = 1 & n2 = width G1 ) or ( |.(n2 - (width G1)).| = 1 & n1 = ma ) )
by A518, SEQM_3:42;
suppose A519:
(
|.(n1 - ma).| = 1 &
n2 = width G1 )
;
contradictionA520:
dom C =
Seg (len C)
by FINSEQ_1:def 3
.=
Seg (len G1)
by MATRIX_0:def 8
.=
dom G1
by FINSEQ_1:def 3
;
then
C /. n1 = C . n1
by A516, PARTFUN1:def 6;
then
(g2 | m) /. lg = C /. n1
by A515, A516, A519, MATRIX_0:def 8;
then A521:
(g2 | m) /. lg in rng C
by A516, A520, PARTFUN2:2;
(g2 | m) /. lg = g2 /. lg
by A13, A24, A17, A489, FINSEQ_4:71;
hence
contradiction
by A13, A17, A489, A507, A521, XREAL_1:44;
verum end; end; end; hence
contradiction
;
verum end; then A524:
pl < len (g2 | m)
by A486, XXREAL_0:1;
len C = len G1
by MATRIX_0:def 8;
then A525:
dom C =
Seg (len G1)
by FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
A526:
Li /. K1 = Li . K1
by A367, PARTFUN1:def 6;
then A527:
(g2 | m) /. pf = G1 * (
mi,
K1)
by A367, A368, A400, MATRIX_0:def 7;
now not pf = len (g2 | m)consider i2 being
Element of
NAT such that A528:
i2 in dom C
and A529:
C /. i2 = (g2 | m) /. (len (g2 | m))
by A28, PARTFUN2:2;
C /. i2 = C . i2
by A528, PARTFUN1:def 6;
then A530:
(g2 | m) /. (len (g2 | m)) = G1 * (
i2,
(width G1))
by A525, A528, A529, MATRIX_0:def 8;
A531:
[i2,(width G1)] in Indices G1
by A73, A96, A525, A528, ZFMISC_1:87;
assume A532:
pf = len (g2 | m)
;
contradictionconsider n1,
n2 being
Nat such that A533:
[n1,n2] in Indices G1
and A534:
(g2 | m) /. lg = G1 * (
n1,
n2)
by A15, A489, GOBOARD1:def 9;
A535:
n1 in dom G1
by A96, A533, ZFMISC_1:87;
A536:
n2 in Seg (width G1)
by A96, A533, ZFMISC_1:87;
[mi,K1] in Indices G1
by A39, A96, A367, A400, ZFMISC_1:87;
then
i2 = mi
by A527, A532, A530, A531, GOBOARD1:5;
then A537:
|.(n1 - mi).| + |.(n2 - (width G1)).| = 1
by A15, A489, A506, A360, A530, A531, A533, A534, GOBOARD1:def 9;
now contradictionper cases
( ( |.(n1 - mi).| = 1 & n2 = width G1 ) or ( |.(n2 - (width G1)).| = 1 & n1 = mi ) )
by A537, SEQM_3:42;
suppose A538:
(
|.(n1 - mi).| = 1 &
n2 = width G1 )
;
contradictionA539:
dom C =
Seg (len C)
by FINSEQ_1:def 3
.=
Seg (len G1)
by MATRIX_0:def 8
.=
dom G1
by FINSEQ_1:def 3
;
then
C /. n1 = C . n1
by A535, PARTFUN1:def 6;
then
(g2 | m) /. lg = C /. n1
by A534, A535, A538, MATRIX_0:def 8;
then A540:
(g2 | m) /. lg in rng C
by A535, A539, PARTFUN2:2;
(g2 | m) /. lg = g2 /. lg
by A13, A24, A17, A489, FINSEQ_4:71;
hence
contradiction
by A13, A17, A489, A507, A540, XREAL_1:44;
verum end; end; end; hence
contradiction
;
verum end; then A543:
pf < len (g2 | m)
by A418, XXREAL_0:1;
now (rng g1) /\ (rng g2) <> {} per cases
( pf < pl or pl < pf )
by A488, XXREAL_0:1;
suppose A544:
pf < pl
;
(rng g1) /\ (rng g2) <> {}
pl <= pl + 1
by NAT_1:11;
then reconsider LL =
(pl + 1) - pf as
Element of
NAT by A544, INT_1:5, XXREAL_0:2;
reconsider w1 =
pf - 1 as
Element of
NAT by A364, INT_1:5;
set F1 =
(g2 | m) | pl;
defpred S11[
Nat,
Element of
(TOP-REAL 2)]
means $2
= ((g2 | m) | pl) /. (w1 + $1);
A545:
for
n being
Nat st
n in Seg LL holds
ex
p being
Point of
(TOP-REAL 2) st
S11[
n,
p]
;
consider F being
FinSequence of
(TOP-REAL 2) such that A546:
(
len F = LL & ( for
n being
Nat st
n in Seg LL holds
S11[
n,
F /. n] ) )
from FINSEQ_4:sch 1(A545);
set hf =
h1 ^ F;
set FF =
(h1 ^ F) ^ h2;
A547:
Seg (len F) = dom F
by FINSEQ_1:def 3;
A548:
for
n being
Nat st
n in Seg LL holds
(
((g2 | m) | pl) /. (w1 + n) = (g2 | m) /. (w1 + n) &
w1 + n in dom (g2 | m) )
A551:
rng F c= rng g2
proof
let x be
object ;
TARSKI:def 3 ( not x in rng F or x in rng g2 )
assume
x in rng F
;
x in rng g2
then consider n being
Element of
NAT such that A552:
n in dom F
and A553:
x = F /. n
by PARTFUN2:2;
F /. n = ((g2 | m) | pl) /. (w1 + n)
by A546, A547, A552;
then A554:
F /. n = (g2 | m) /. (w1 + n)
by A548, A546, A547, A552;
w1 + n in dom (g2 | m)
by A548, A546, A547, A552;
then
x in rng (g2 | m)
by A553, A554, PARTFUN2:2;
hence
x in rng g2
by A18;
verum
end;
pf + 1
<= pl
by A544, NAT_1:13;
then
pf + 1
<= pl + 1
by NAT_1:13;
then A555:
1
<= LL
by XREAL_1:19;
A556:
now for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ F) /. (len (h1 ^ F)) = G1 * (i1,i2) & h2 /. 1 = G1 * (j1,j2) & len (h1 ^ F) in dom (h1 ^ F) & 1 in dom h2 holds
|.(i1 - j1).| + |.(i2 - j2).| = 1let i1,
i2,
j1,
j2 be
Nat;
( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ F) /. (len (h1 ^ F)) = G1 * (i1,i2) & h2 /. 1 = G1 * (j1,j2) & len (h1 ^ F) in dom (h1 ^ F) & 1 in dom h2 implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A557:
[i1,i2] in Indices G1
and A558:
[j1,j2] in Indices G1
and A559:
(h1 ^ F) /. (len (h1 ^ F)) = G1 * (
i1,
i2)
and A560:
h2 /. 1
= G1 * (
j1,
j2)
and
len (h1 ^ F) in dom (h1 ^ F)
and A561:
1
in dom h2
;
|.(i1 - j1).| + |.(i2 - j2).| = 1
ma + 1
in dom G1
by A469, A561;
then A562:
[(ma + 1),K2] in Indices G1
by A96, A365, A355, ZFMISC_1:87;
A563:
[ma,K2] in Indices G1
by A41, A96, A365, A355, ZFMISC_1:87;
A564:
len F in dom F
by A546, A547, A555, FINSEQ_1:1;
(h1 ^ F) /. (len (h1 ^ F)) =
(h1 ^ F) /. ((len h1) + (len F))
by FINSEQ_1:22
.=
F /. (len F)
by A564, FINSEQ_4:69
.=
((g2 | m) | pl) /. (w1 + LL)
by A546, A547, A564
.=
G1 * (
ma,
K2)
by A420, A548, A546, A547, A564
;
then A565:
(
i1 = ma &
i2 = K2 )
by A557, A559, A563, GOBOARD1:5;
h2 /. 1
= G1 * (
(ma + 1),
K2)
by A421, A561;
then
(
j1 = ma + 1 &
j2 = K2 )
by A558, A560, A562, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| =
|.(ma - (ma + 1)).| + 0
by A565, ABSVALUE:2
.=
|.(- ((ma + 1) - ma)).|
.=
|.1.|
by COMPLEX1:52
.=
1
by ABSVALUE:def 1
;
verum end; A566:
rng ((h1 ^ F) ^ h2) =
(rng (h1 ^ F)) \/ (rng h2)
by FINSEQ_1:31
.=
((rng h1) \/ (rng F)) \/ (rng h2)
by FINSEQ_1:31
;
A567:
for
k being
Nat st
k in Seg (width G1) &
(rng F) /\ (rng (Col (G1,k))) = {} holds
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {}
proof
A568:
len (Col (G1,K2)) = len G1
by MATRIX_0:def 8;
A569:
len (Col (G1,K1)) = len G1
by MATRIX_0:def 8;
let k be
Nat;
( k in Seg (width G1) & (rng F) /\ (rng (Col (G1,k))) = {} implies (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {} )
assume that A570:
k in Seg (width G1)
and A571:
(rng F) /\ (rng (Col (G1,k))) = {}
;
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {}
set gg =
Col (
G1,
k);
assume A572:
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) <> {}
;
contradiction
set x = the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k)));
rng ((h1 ^ F) ^ h2) = (rng F) \/ ((rng h1) \/ (rng h2))
by A566, XBOOLE_1:4;
then A573:
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) =
{} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col (G1,k))))
by A571, XBOOLE_1:23
.=
((rng h1) /\ (rng (Col (G1,k)))) \/ ((rng h2) /\ (rng (Col (G1,k))))
by XBOOLE_1:23
;
now contradictionper cases
( the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k))) or the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k))) )
by A572, A573, XBOOLE_0:def 3;
suppose A574:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k)))
;
contradictionthen
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng h1
by XBOOLE_0:def 4;
then consider i being
Element of
NAT such that A575:
i in dom h1
and A576:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = h1 /. i
by PARTFUN2:2;
A577:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = G1 * (
i,
K1)
by A369, A575, A576;
reconsider y = the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) as
Point of
(TOP-REAL 2) by A576;
A578:
Lmi /. K1 = Lmi . K1
by A367, PARTFUN1:def 6;
A579:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k))
by A574, XBOOLE_0:def 4;
A580:
dom CK1 =
Seg (len G1)
by A569, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
then A581:
CK1 /. mi = CK1 . mi
by A39, PARTFUN1:def 6;
A582:
i in dom CK1
by A401, A575, A580;
CK1 /. i = CK1 . i
by A401, A575, A580, PARTFUN1:def 6;
then
y = CK1 /. i
by A577, A580, A582, MATRIX_0:def 8;
then
y in rng CK1
by A582, PARTFUN2:2;
then A583:
K1 = k
by A367, A400, A570, A579, GOBOARD1:4;
A584:
1
in Seg LL
by A555, FINSEQ_1:1;
then
(
F /. 1
= ((g2 | m) | pl) /. (w1 + 1) &
((g2 | m) | pl) /. (w1 + 1) = (g2 | m) /. (w1 + 1) )
by A548, A546;
then
F /. 1
= CK1 /. mi
by A39, A367, A368, A400, A578, A581, MATRIX_0:42;
then A585:
F /. 1
in rng (Col (G1,k))
by A39, A580, A583, PARTFUN2:2;
F /. 1
in rng F
by A546, A547, A584, PARTFUN2:2;
hence
contradiction
by A571, A585, XBOOLE_0:def 4;
verum end; suppose A586:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k)))
;
contradictionthen
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng h2
by XBOOLE_0:def 4;
then consider i being
Element of
NAT such that A587:
i in dom h2
and A588:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = h2 /. i
by PARTFUN2:2;
A589:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = G1 * (
(ma + i),
K2)
by A421, A587, A588;
reconsider y = the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) as
Point of
(TOP-REAL 2) by A588;
A590:
Lma /. K2 = Lma . K2
by A365, PARTFUN1:def 6;
A591:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k))
by A586, XBOOLE_0:def 4;
A592:
dom CK2 =
Seg (len G1)
by A568, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
then A593:
CK2 /. ma = CK2 . ma
by A41, PARTFUN1:def 6;
A594:
ma + i in dom CK2
by A469, A587, A592;
CK2 /. (ma + i) = CK2 . (ma + i)
by A469, A587, A592, PARTFUN1:def 6;
then
y = CK2 /. (ma + i)
by A589, A592, A594, MATRIX_0:def 8;
then
y in rng CK2
by A594, PARTFUN2:2;
then A595:
K2 = k
by A365, A355, A570, A591, GOBOARD1:4;
A596:
LL in Seg LL
by A555, FINSEQ_1:1;
then
(
F /. LL = ((g2 | m) | pl) /. (w1 + LL) &
((g2 | m) | pl) /. (w1 + LL) = (g2 | m) /. (w1 + LL) )
by A548, A546;
then
F /. LL = CK2 /. ma
by A41, A365, A366, A355, A590, A593, MATRIX_0:42;
then A597:
F /. LL in rng (Col (G1,k))
by A41, A592, A595, PARTFUN2:2;
F /. LL in rng F
by A546, A547, A596, PARTFUN2:2;
hence
contradiction
by A571, A597, XBOOLE_0:def 4;
verum end; end; end;
hence
contradiction
;
verum
end;
(rng F) /\ (rng C) = {}
proof
reconsider w =
w1 as
Nat ;
set x = the
Element of
(rng F) /\ (rng C);
assume A598:
not
(rng F) /\ (rng C) = {}
;
contradiction
then A599:
the
Element of
(rng F) /\ (rng C) in rng C
by XBOOLE_0:def 4;
the
Element of
(rng F) /\ (rng C) in rng F
by A598, XBOOLE_0:def 4;
then consider i1 being
Element of
NAT such that A600:
i1 in dom F
and A601:
F /. i1 = the
Element of
(rng F) /\ (rng C)
by PARTFUN2:2;
A602:
Seg (len F) = dom F
by FINSEQ_1:def 3;
then
i1 <= LL
by A546, A600, FINSEQ_1:1;
then A603:
w + i1 <= w + LL
by XREAL_1:7;
A604:
w1 + i1 in dom (g2 | m)
by A548, A546, A600, A602;
then A605:
w + i1 in dom g2
by A13, A24, A17, FINSEQ_4:71;
(
F /. i1 = ((g2 | m) | pl) /. (w1 + i1) &
((g2 | m) | pl) /. (w1 + i1) = (g2 | m) /. (w1 + i1) )
by A548, A546, A600, A602;
then
g2 /. (w + i1) in rng C
by A13, A24, A17, A599, A601, A604, FINSEQ_4:71;
then
m <= w + i1
by A13, A605;
hence
contradiction
by A17, A524, A603, XXREAL_0:2;
verum
end; then
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,(width G1)))) = {}
by A73, A567;
then A606:
rng ((h1 ^ F) ^ h2) misses rng (Col (G1,(width G1)))
by XBOOLE_0:def 7;
now for n being Nat st n in dom F holds
ex i, j being Nat st
( [i,j] in Indices G1 & F /. n = G1 * (i,j) )reconsider w =
w1 as
Nat ;
let n be
Nat;
( n in dom F implies ex i, j being Nat st
( [i,j] in Indices G1 & F /. n = G1 * (i,j) ) )assume A607:
n in dom F
;
ex i, j being Nat st
( [i,j] in Indices G1 & F /. n = G1 * (i,j) )then
w1 + n in dom (g2 | m)
by A548, A546, A547;
then consider i,
j being
Nat such that A608:
(
[i,j] in Indices G1 &
(g2 | m) /. (w + n) = G1 * (
i,
j) )
by A15, GOBOARD1:def 9;
take i =
i;
ex j being Nat st
( [i,j] in Indices G1 & F /. n = G1 * (i,j) )take j =
j;
( [i,j] in Indices G1 & F /. n = G1 * (i,j) )
F /. n = ((g2 | m) | pl) /. (w1 + n)
by A546, A547, A607;
hence
(
[i,j] in Indices G1 &
F /. n = G1 * (
i,
j) )
by A548, A546, A547, A607, A608;
verum end; then
for
n being
Nat st
n in dom (h1 ^ F) holds
ex
i,
j being
Nat st
(
[i,j] in Indices G1 &
(h1 ^ F) /. n = G1 * (
i,
j) )
by A406, GOBOARD1:23;
then A609:
for
n being
Nat st
n in dom ((h1 ^ F) ^ h2) holds
ex
i,
j being
Nat st
(
[i,j] in Indices G1 &
((h1 ^ F) ^ h2) /. n = G1 * (
i,
j) )
by A473, GOBOARD1:23;
A610:
now for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. (len h1) = G1 * (i1,i2) & F /. 1 = G1 * (j1,j2) & len h1 in dom h1 & 1 in dom F holds
|.(i1 - j1).| + |.(i2 - j2).| = 1A611:
[mi,K1] in Indices G1
by A39, A96, A367, A400, ZFMISC_1:87;
let i1,
i2,
j1,
j2 be
Nat;
( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. (len h1) = G1 * (i1,i2) & F /. 1 = G1 * (j1,j2) & len h1 in dom h1 & 1 in dom F implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A612:
[i1,i2] in Indices G1
and A613:
[j1,j2] in Indices G1
and A614:
h1 /. (len h1) = G1 * (
i1,
i2)
and A615:
F /. 1
= G1 * (
j1,
j2)
and A616:
len h1 in dom h1
and A617:
1
in dom F
;
|.(i1 - j1).| + |.(i2 - j2).| = 1
F /. 1
= ((g2 | m) | pl) /. (w1 + 1)
by A546, A547, A617;
then F /. 1 =
(g2 | m) /. (w1 + 1)
by A548, A546, A547, A617
.=
G1 * (
mi,
K1)
by A367, A368, A400, A526, MATRIX_0:def 7
;
then A618:
(
j1 = mi &
j2 = K1 )
by A613, A615, A611, GOBOARD1:5;
l1 in dom G1
by A369, A401, A616;
then A619:
[l1,K1] in Indices G1
by A96, A367, A400, ZFMISC_1:87;
h1 /. (len h1) = G1 * (
l1,
K1)
by A369, A616;
then
(
i1 = l1 &
i2 = K1 )
by A612, A614, A619, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| =
|.((mi - 1) - mi).| + 0
by A618, ABSVALUE:2
.=
|.(- 1).|
.=
|.1.|
by COMPLEX1:52
.=
1
by ABSVALUE:def 1
;
verum end; now for n being Nat st n in dom F & n + 1 in dom F holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1let n be
Nat;
( n in dom F & n + 1 in dom F implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A620:
n in dom F
and A621:
n + 1
in dom F
;
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
F /. n = ((g2 | m) | pl) /. (w1 + n)
by A546, A547, A620;
then A622:
F /. n = (g2 | m) /. (w1 + n)
by A548, A546, A547, A620;
F /. (n + 1) = ((g2 | m) | pl) /. (w1 + (n + 1))
by A546, A547, A621;
then A623:
(
(w1 + n) + 1
in dom (g2 | m) &
F /. (n + 1) = (g2 | m) /. ((w1 + n) + 1) )
by A548, A546, A547, A621;
let i1,
i2,
j1,
j2 be
Nat;
( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )assume A624:
(
[i1,i2] in Indices G1 &
[j1,j2] in Indices G1 &
F /. n = G1 * (
i1,
i2) &
F /. (n + 1) = G1 * (
j1,
j2) )
;
|.(i1 - j1).| + |.(i2 - j2).| = 1
w1 + n in dom (g2 | m)
by A548, A546, A547, A620;
hence
|.(i1 - j1).| + |.(i2 - j2).| = 1
by A15, A622, A623, A624, GOBOARD1:def 9;
verum end; then
for
n being
Nat st
n in dom (h1 ^ F) &
n + 1
in dom (h1 ^ F) holds
for
i1,
i2,
j1,
j2 being
Nat st
[i1,i2] in Indices G1 &
[j1,j2] in Indices G1 &
(h1 ^ F) /. n = G1 * (
i1,
i2) &
(h1 ^ F) /. (n + 1) = G1 * (
j1,
j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
by A408, A610, GOBOARD1:24;
then
for
n being
Nat st
n in dom ((h1 ^ F) ^ h2) &
n + 1
in dom ((h1 ^ F) ^ h2) holds
for
i1,
i2,
j1,
j2 being
Nat st
[i1,i2] in Indices G1 &
[j1,j2] in Indices G1 &
((h1 ^ F) ^ h2) /. n = G1 * (
i1,
i2) &
((h1 ^ F) ^ h2) /. (n + 1) = G1 * (
j1,
j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
by A475, A556, GOBOARD1:24;
then
(h1 ^ F) ^ h2 is_sequence_on G1
by A609, GOBOARD1:def 9;
then A625:
(h1 ^ F) ^ h2 is_sequence_on DelCol (
G1,
(width G1))
by A73, A152, A606, GOBOARD1:25;
set x = the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng tt);
A626:
0 + 1
<= (len F) + ((len h1) + (len h2))
by A546, A555, XREAL_1:7;
A627:
now ((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1))per cases
( mi = 1 or mi <> 1 )
;
suppose A628:
mi = 1
;
((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1))A629:
pf in Seg pl
by A364, A544, FINSEQ_1:1;
A630:
1
in Seg LL
by A555, FINSEQ_1:1;
h1 = {}
by A369, A628;
then
(h1 ^ F) ^ h2 = F ^ h2
by FINSEQ_1:34;
then ((h1 ^ F) ^ h2) /. 1 =
F /. 1
by A546, A547, A630, FINSEQ_4:68
.=
((g2 | m) | pl) /. (w1 + 1)
by A546, A630
.=
(g2 | m) /. pf
by A363, A629, FINSEQ_4:71
;
hence
((h1 ^ F) ^ h2) /. 1
in rng (Line (G1,1))
by A359, A628;
verum end; suppose A631:
mi <> 1
;
((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1))
1
<= mi
by A39, FINSEQ_3:25;
then
1
< mi
by A631, XXREAL_0:1;
then
1
+ 1
<= mi
by NAT_1:13;
then A632:
1
<= l1
by XREAL_1:19;
then A633:
1
in Seg l1
by FINSEQ_1:1;
len (Line (G1,1)) = width G1
by MATRIX_0:def 7;
then A634:
K1 in dom L1
by A367, A400, FINSEQ_1:def 3;
then A635:
L1 /. K1 = L1 . K1
by PARTFUN1:def 6;
(
len (h1 ^ F) = (len h1) + (len F) &
0 <= len F )
by FINSEQ_1:22;
then
0 + 1
<= len (h1 ^ F)
by A369, A632, XREAL_1:7;
then
1
in dom (h1 ^ F)
by FINSEQ_3:25;
then ((h1 ^ F) ^ h2) /. 1 =
(h1 ^ F) /. 1
by FINSEQ_4:68
.=
h1 /. 1
by A369, A468, A633, FINSEQ_4:68
.=
G1 * (1,
K1)
by A369, A468, A633
.=
L1 /. K1
by A367, A400, A635, MATRIX_0:def 7
;
hence
((h1 ^ F) ^ h2) /. 1
in rng (Line (G1,1))
by A634, PARTFUN2:2;
verum end; end; end; A636:
w1 + LL = pl
;
A637:
now ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1)))per cases
( ma = len G1 or ma <> len G1 )
;
suppose A638:
ma = len G1
;
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1)))
1
<= pl
by A24, A363, FINSEQ_1:1;
then A639:
pl in Seg pl
by FINSEQ_1:1;
A640:
len F in dom F
by A546, A555, FINSEQ_3:25;
h2 = {}
by A421, A638;
then A641:
(h1 ^ F) ^ h2 = h1 ^ F
by FINSEQ_1:34;
then ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) =
((h1 ^ F) ^ h2) /. ((len h1) + (len F))
by FINSEQ_1:22
.=
F /. LL
by A546, A641, A640, FINSEQ_4:69
.=
((g2 | m) | pl) /. pl
by A546, A547, A636, A640
.=
(g2 | m) /. pl
by A363, A639, FINSEQ_4:71
;
hence
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1)))
by A363, A638;
verum end; suppose A642:
ma <> len G1
;
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1)))
ma <= len G1
by A41, FINSEQ_3:25;
then
ma < len G1
by A642, XXREAL_0:1;
then
ma + 1
<= len G1
by NAT_1:13;
then A643:
1
<= l2
by XREAL_1:19;
then A644:
l2 in Seg l2
by FINSEQ_1:1;
len (Line (G1,(len G1))) = width G1
by MATRIX_0:def 7;
then A645:
K2 in dom Ll
by A365, A355, FINSEQ_1:def 3;
then A646:
Ll /. K2 = Ll . K2
by PARTFUN1:def 6;
A647:
len h2 in dom h2
by A421, A643, FINSEQ_3:25;
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) =
((h1 ^ F) ^ h2) /. ((len (h1 ^ F)) + (len h2))
by FINSEQ_1:22
.=
h2 /. l2
by A421, A647, FINSEQ_4:69
.=
G1 * (
(ma + l2),
K2)
by A421, A485, A644
.=
Ll /. K2
by A365, A355, A646, MATRIX_0:def 7
;
hence
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1)))
by A645, PARTFUN2:2;
verum end; end; end;
rng tt c= rng f
by A351, A354;
then A648:
rng tt c= rng g1
by A178;
A649:
len ((h1 ^ F) ^ h2) =
(len (h1 ^ F)) + (len h2)
by FINSEQ_1:22
.=
((len h1) + (len F)) + (len h2)
by FINSEQ_1:22
;
then
1
in dom ((h1 ^ F) ^ h2)
by A626, FINSEQ_3:25;
then A650:
((h1 ^ F) ^ h2) /. 1
in rng (Line ((DelCol (G1,(width G1))),1))
by A73, A26, A152, A627, A606, MATRIX_0:75;
len ((h1 ^ F) ^ h2) in dom ((h1 ^ F) ^ h2)
by A649, A626, FINSEQ_3:25;
then A651:
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line ((DelCol (G1,(width G1))),(len (DelCol (G1,(width G1))))))
by A73, A27, A152, A153, A637, A606, MATRIX_0:75;
width (DelCol (G1,(width G1))) = k
by A3, A73, MATRIX_0:63;
then
(rng ((h1 ^ F) ^ h2)) /\ (rng tt) <> {}
by A2, A92, A353, A649, A626, A625, A650, A651, A341;
then A652:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng tt) in (rng ((h1 ^ F) ^ h2)) /\ (rng tt)
;
(rng tt) /\ (rng ((h1 ^ F) ^ h2)) =
(((rng h1) \/ (rng F)) /\ (rng tt)) \/ {}
by A492, A566, XBOOLE_1:23
.=
{} \/ ((rng F) /\ (rng tt))
by A424, XBOOLE_1:23
.=
(rng tt) /\ (rng F)
;
then
(rng ((h1 ^ F) ^ h2)) /\ (rng tt) c= (rng g1) /\ (rng g2)
by A648, A551, XBOOLE_1:27;
hence
(rng g1) /\ (rng g2) <> {}
by A652;
verum end; suppose A653:
pl < pf
;
(rng g1) /\ (rng g2) <> {}
pf <= pf + 1
by NAT_1:11;
then reconsider LL =
(pf + 1) - pl as
Element of
NAT by A653, INT_1:5, XXREAL_0:2;
set F1 =
(g2 | m) | pf;
defpred S11[
Nat,
Element of
(TOP-REAL 2)]
means for
k being
Nat st
k = (pf + 1) - $1 holds
$2
= ((g2 | m) | pf) /. k;
A654:
for
n,
k being
Nat st
n in Seg LL &
k = (pf + 1) - n holds
(
((g2 | m) | pf) /. k = (g2 | m) /. k &
k in dom (g2 | m) )
proof
let n,
k be
Nat;
( n in Seg LL & k = (pf + 1) - n implies ( ((g2 | m) | pf) /. k = (g2 | m) /. k & k in dom (g2 | m) ) )
assume that A655:
n in Seg LL
and A656:
k = (pf + 1) - n
;
( ((g2 | m) | pf) /. k = (g2 | m) /. k & k in dom (g2 | m) )
A657:
n <= LL
by A655, FINSEQ_1:1;
1
<= n
by A655, FINSEQ_1:1;
then A658:
(pf + 1) - n <= (pf + 1) - 1
by XREAL_1:13;
LL <= (pf + 1) - 0
by XREAL_1:13;
then reconsider w =
(pf + 1) - n as
Element of
NAT by A657, INT_1:5, XXREAL_0:2;
(pf + 1) - LL <= (pf + 1) - n
by A657, XREAL_1:13;
then
1
<= (pf + 1) - n
by A487, XXREAL_0:2;
then
w in Seg pf
by A658, FINSEQ_1:1;
hence
(
((g2 | m) | pf) /. k = (g2 | m) /. k &
k in dom (g2 | m) )
by A359, A656, FINSEQ_4:71;
verum
end; A659:
for
n being
Nat st
n in Seg LL holds
(pf + 1) - n is
Element of
NAT
A661:
for
n being
Nat st
n in Seg LL holds
ex
p being
Point of
(TOP-REAL 2) st
S11[
n,
p]
consider F being
FinSequence of
(TOP-REAL 2) such that A663:
(
len F = LL & ( for
n being
Nat st
n in Seg LL holds
S11[
n,
F /. n] ) )
from FINSEQ_4:sch 1(A661);
set hf =
h1 ^ F;
set FF =
(h1 ^ F) ^ h2;
A664:
Seg (len F) = dom F
by FINSEQ_1:def 3;
A665:
rng F c= rng g2
pl + 1
<= pf
by A653, NAT_1:13;
then
pl + 1
<= pf + 1
by NAT_1:13;
then A668:
1
<= LL
by XREAL_1:19;
A669:
now for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ F) /. (len (h1 ^ F)) = G1 * (i1,i2) & h2 /. 1 = G1 * (j1,j2) & len (h1 ^ F) in dom (h1 ^ F) & 1 in dom h2 holds
|.(i1 - j1).| + |.(i2 - j2).| = 1reconsider u =
(pf + 1) - LL as
Nat ;
let i1,
i2,
j1,
j2 be
Nat;
( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ F) /. (len (h1 ^ F)) = G1 * (i1,i2) & h2 /. 1 = G1 * (j1,j2) & len (h1 ^ F) in dom (h1 ^ F) & 1 in dom h2 implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A670:
[i1,i2] in Indices G1
and A671:
[j1,j2] in Indices G1
and A672:
(h1 ^ F) /. (len (h1 ^ F)) = G1 * (
i1,
i2)
and A673:
h2 /. 1
= G1 * (
j1,
j2)
and
len (h1 ^ F) in dom (h1 ^ F)
and A674:
1
in dom h2
;
|.(i1 - j1).| + |.(i2 - j2).| = 1
ma + 1
in dom G1
by A469, A674;
then A675:
[(ma + 1),K2] in Indices G1
by A96, A365, A355, ZFMISC_1:87;
A676:
[ma,K2] in Indices G1
by A41, A96, A365, A355, ZFMISC_1:87;
A677:
len F in dom F
by A663, A668, FINSEQ_3:25;
(h1 ^ F) /. (len (h1 ^ F)) =
(h1 ^ F) /. ((len h1) + (len F))
by FINSEQ_1:22
.=
F /. (len F)
by A677, FINSEQ_4:69
.=
((g2 | m) | pf) /. u
by A663, A664, A677
.=
(g2 | m) /. u
by A654, A663, A664, A677
.=
G1 * (
ma,
K2)
by A365, A366, A355, A419, MATRIX_0:def 7
;
then A678:
(
i1 = ma &
i2 = K2 )
by A670, A672, A676, GOBOARD1:5;
h2 /. 1
= G1 * (
(ma + 1),
K2)
by A421, A674;
then
(
j1 = ma + 1 &
j2 = K2 )
by A671, A673, A675, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| =
|.(ma - (ma + 1)).| + 0
by A678, ABSVALUE:2
.=
|.(- ((ma + 1) - ma)).|
.=
|.1.|
by COMPLEX1:52
.=
1
by ABSVALUE:def 1
;
verum end; now for n being Nat st n in dom F holds
ex i, j being Nat st
( [i,j] in Indices G1 & F /. n = G1 * (i,j) )let n be
Nat;
( n in dom F implies ex i, j being Nat st
( [i,j] in Indices G1 & F /. n = G1 * (i,j) ) )assume A679:
n in dom F
;
ex i, j being Nat st
( [i,j] in Indices G1 & F /. n = G1 * (i,j) )then reconsider w =
(pf + 1) - n as
Nat by A659, A663, A664;
A680:
F /. n = ((g2 | m) | pf) /. w
by A663, A664, A679;
then
(pf + 1) - n in dom (g2 | m)
by A654, A663, A664, A679;
then consider i,
j being
Nat such that A681:
(
[i,j] in Indices G1 &
(g2 | m) /. w = G1 * (
i,
j) )
by A15, GOBOARD1:def 9;
take i =
i;
ex j being Nat st
( [i,j] in Indices G1 & F /. n = G1 * (i,j) )take j =
j;
( [i,j] in Indices G1 & F /. n = G1 * (i,j) )thus
(
[i,j] in Indices G1 &
F /. n = G1 * (
i,
j) )
by A654, A663, A664, A679, A680, A681;
verum end; then
for
n being
Nat st
n in dom (h1 ^ F) holds
ex
i,
j being
Nat st
(
[i,j] in Indices G1 &
(h1 ^ F) /. n = G1 * (
i,
j) )
by A406, GOBOARD1:23;
then A682:
for
n being
Nat st
n in dom ((h1 ^ F) ^ h2) holds
ex
i,
j being
Nat st
(
[i,j] in Indices G1 &
((h1 ^ F) ^ h2) /. n = G1 * (
i,
j) )
by A473, GOBOARD1:23;
set x = the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng tt);
A683:
0 + 1
<= (len F) + ((len h1) + (len h2))
by A663, A668, XREAL_1:7;
A684:
rng ((h1 ^ F) ^ h2) =
(rng (h1 ^ F)) \/ (rng h2)
by FINSEQ_1:31
.=
((rng h1) \/ (rng F)) \/ (rng h2)
by FINSEQ_1:31
;
A685:
for
k being
Nat st
k in Seg (width G1) &
(rng F) /\ (rng (Col (G1,k))) = {} holds
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {}
proof
A686:
len (Col (G1,K2)) = len G1
by MATRIX_0:def 8;
A687:
len (Col (G1,K1)) = len G1
by MATRIX_0:def 8;
let k be
Nat;
( k in Seg (width G1) & (rng F) /\ (rng (Col (G1,k))) = {} implies (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {} )
assume that A688:
k in Seg (width G1)
and A689:
(rng F) /\ (rng (Col (G1,k))) = {}
;
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {}
set gg =
Col (
G1,
k);
assume A690:
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) <> {}
;
contradiction
set x = the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k)));
rng ((h1 ^ F) ^ h2) = (rng F) \/ ((rng h1) \/ (rng h2))
by A684, XBOOLE_1:4;
then A691:
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) =
{} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col (G1,k))))
by A689, XBOOLE_1:23
.=
((rng h1) /\ (rng (Col (G1,k)))) \/ ((rng h2) /\ (rng (Col (G1,k))))
by XBOOLE_1:23
;
now contradictionper cases
( the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k))) or the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k))) )
by A690, A691, XBOOLE_0:def 3;
suppose A692:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k)))
;
contradictionthen A693:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k))
by XBOOLE_0:def 4;
A694:
1
in Seg LL
by A668, FINSEQ_1:1;
(pf + 1) - 1
= pf
;
then A695:
(
F /. 1
= ((g2 | m) | pf) /. pf &
((g2 | m) | pf) /. pf = (g2 | m) /. pf )
by A654, A663, A694;
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng h1
by A692, XBOOLE_0:def 4;
then consider i being
Element of
NAT such that A696:
i in dom h1
and A697:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = h1 /. i
by PARTFUN2:2;
A698:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = G1 * (
i,
K1)
by A369, A696, A697;
reconsider y = the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) as
Point of
(TOP-REAL 2) by A697;
A699:
Lmi /. K1 = Lmi . K1
by A367, PARTFUN1:def 6;
A700:
dom CK1 =
Seg (len G1)
by A687, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
then A701:
i in dom CK1
by A401, A696;
CK1 /. i = CK1 . i
by A401, A696, A700, PARTFUN1:def 6;
then
y = CK1 /. i
by A698, A700, A701, MATRIX_0:def 8;
then
y in rng CK1
by A701, PARTFUN2:2;
then A702:
K1 = k
by A367, A400, A688, A693, GOBOARD1:4;
CK1 /. mi = CK1 . mi
by A39, A700, PARTFUN1:def 6;
then
F /. 1
= CK1 /. mi
by A39, A367, A368, A400, A699, A695, MATRIX_0:42;
then A703:
F /. 1
in rng (Col (G1,k))
by A39, A700, A702, PARTFUN2:2;
F /. 1
in rng F
by A663, A664, A694, PARTFUN2:2;
hence
contradiction
by A689, A703, XBOOLE_0:def 4;
verum end; suppose A704:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k)))
;
contradictionthen
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng h2
by XBOOLE_0:def 4;
then consider i being
Element of
NAT such that A705:
i in dom h2
and A706:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = h2 /. i
by PARTFUN2:2;
A707:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = G1 * (
(ma + i),
K2)
by A421, A705, A706;
reconsider y = the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) as
Point of
(TOP-REAL 2) by A706;
A708:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k))
by A704, XBOOLE_0:def 4;
reconsider u =
(pf + 1) - LL as
Nat ;
A709:
Lma /. K2 = Lma . K2
by A365, PARTFUN1:def 6;
A710:
dom CK2 =
Seg (len G1)
by A686, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
then A711:
CK2 /. ma = CK2 . ma
by A41, PARTFUN1:def 6;
A712:
ma + i in dom CK2
by A469, A705, A710;
CK2 /. (ma + i) = CK2 . (ma + i)
by A469, A705, A710, PARTFUN1:def 6;
then
y = CK2 /. (ma + i)
by A707, A710, A712, MATRIX_0:def 8;
then
y in rng CK2
by A712, PARTFUN2:2;
then A713:
K2 = k
by A365, A355, A688, A708, GOBOARD1:4;
A714:
LL in Seg LL
by A668, FINSEQ_1:1;
then
(
F /. LL = ((g2 | m) | pf) /. u &
((g2 | m) | pf) /. u = (g2 | m) /. u )
by A654, A663;
then
F /. LL = CK2 /. ma
by A41, A365, A366, A355, A709, A711, MATRIX_0:42;
then A715:
F /. LL in rng (Col (G1,k))
by A41, A710, A713, PARTFUN2:2;
F /. LL in rng F
by A663, A664, A714, PARTFUN2:2;
hence
contradiction
by A689, A715, XBOOLE_0:def 4;
verum end; end; end;
hence
contradiction
;
verum
end;
(rng F) /\ (rng C) = {}
proof
set x = the
Element of
(rng F) /\ (rng C);
assume A716:
not
(rng F) /\ (rng C) = {}
;
contradiction
then A717:
the
Element of
(rng F) /\ (rng C) in rng C
by XBOOLE_0:def 4;
the
Element of
(rng F) /\ (rng C) in rng F
by A716, XBOOLE_0:def 4;
then consider i1 being
Element of
NAT such that A718:
i1 in dom F
and A719:
F /. i1 = the
Element of
(rng F) /\ (rng C)
by PARTFUN2:2;
reconsider w =
(pf + 1) - i1 as
Nat by A659, A663, A664, A718;
1
<= i1
by A718, FINSEQ_3:25;
then A720:
w <= (pf + 1) - 1
by XREAL_1:13;
A721:
w in dom (g2 | m)
by A654, A663, A664, A718;
then A722:
w in dom g2
by A13, A24, A17, FINSEQ_4:71;
(
F /. i1 = ((g2 | m) | pf) /. w &
((g2 | m) | pf) /. w = (g2 | m) /. w )
by A654, A663, A664, A718;
then
g2 /. w in rng C
by A13, A24, A17, A717, A719, A721, FINSEQ_4:71;
then
m <= w
by A13, A722;
hence
contradiction
by A17, A543, A720, XXREAL_0:2;
verum
end; then
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,(width G1)))) = {}
by A73, A685;
then A723:
rng ((h1 ^ F) ^ h2) misses rng (Col (G1,(width G1)))
by XBOOLE_0:def 7;
A724:
now for n being Nat st n in dom F & n + 1 in dom F holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) holds
1 = |.(i1 - j1).| + |.(i2 - j2).|let n be
Nat;
( n in dom F & n + 1 in dom F implies for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) holds
1 = |.(i1 - j1).| + |.(i2 - j2).| )assume that A725:
n in dom F
and A726:
n + 1
in dom F
;
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) holds
1 = |.(i1 - j1).| + |.(i2 - j2).|reconsider w3 =
(pf + 1) - n,
w2 =
(pf + 1) - (n + 1) as
Element of
NAT by A659, A663, A664, A725, A726;
F /. n = ((g2 | m) | pf) /. w3
by A663, A664, A725;
then A727:
(
(pf + 1) - n in dom (g2 | m) &
F /. n = (g2 | m) /. w3 )
by A654, A663, A664, A725;
F /. (n + 1) = ((g2 | m) | pf) /. w2
by A663, A664, A726;
then A728:
(
(pf + 1) - (n + 1) in dom (g2 | m) &
F /. (n + 1) = (g2 | m) /. w2 )
by A654, A663, A664, A726;
let i1,
i2,
j1,
j2 be
Nat;
( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) implies 1 = |.(i1 - j1).| + |.(i2 - j2).| )assume A729:
(
[i1,i2] in Indices G1 &
[j1,j2] in Indices G1 &
F /. n = G1 * (
i1,
i2) &
F /. (n + 1) = G1 * (
j1,
j2) )
;
1 = |.(i1 - j1).| + |.(i2 - j2).|
w2 + 1
= (pf + 1) - n
;
hence 1 =
|.(j1 - i1).| + |.(j2 - i2).|
by A15, A727, A728, A729, GOBOARD1:def 9
.=
|.(- (i1 - j1)).| + |.(- (i2 - j2)).|
.=
|.(i1 - j1).| + |.(- (i2 - j2)).|
by COMPLEX1:52
.=
|.(i1 - j1).| + |.(i2 - j2).|
by COMPLEX1:52
;
verum end; A730:
(pf + 1) - 1
= pf
;
A731:
now ((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1))per cases
( mi = 1 or mi <> 1 )
;
suppose A732:
mi = 1
;
((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1))A733:
pf in Seg pf
by A364, FINSEQ_1:1;
A734:
1
in Seg LL
by A668, FINSEQ_1:1;
h1 = {}
by A369, A732;
then
(h1 ^ F) ^ h2 = F ^ h2
by FINSEQ_1:34;
then ((h1 ^ F) ^ h2) /. 1 =
F /. 1
by A663, A664, A734, FINSEQ_4:68
.=
((g2 | m) | pf) /. pf
by A663, A730, A734
.=
(g2 | m) /. pf
by A359, A733, FINSEQ_4:71
;
hence
((h1 ^ F) ^ h2) /. 1
in rng (Line (G1,1))
by A359, A732;
verum end; suppose A735:
mi <> 1
;
((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1))
1
<= mi
by A39, FINSEQ_3:25;
then
1
< mi
by A735, XXREAL_0:1;
then
1
+ 1
<= mi
by NAT_1:13;
then A736:
1
<= l1
by XREAL_1:19;
then A737:
1
in Seg l1
by FINSEQ_1:1;
len (Line (G1,1)) = width G1
by MATRIX_0:def 7;
then A738:
K1 in dom L1
by A367, A400, FINSEQ_1:def 3;
then A739:
L1 /. K1 = L1 . K1
by PARTFUN1:def 6;
(
len (h1 ^ F) = (len h1) + (len F) &
0 <= len F )
by FINSEQ_1:22;
then
0 + 1
<= len (h1 ^ F)
by A369, A736, XREAL_1:7;
then
1
in dom (h1 ^ F)
by FINSEQ_3:25;
then ((h1 ^ F) ^ h2) /. 1 =
(h1 ^ F) /. 1
by FINSEQ_4:68
.=
h1 /. 1
by A369, A468, A737, FINSEQ_4:68
.=
G1 * (1,
K1)
by A369, A468, A737
.=
L1 /. K1
by A367, A400, A739, MATRIX_0:def 7
;
hence
((h1 ^ F) ^ h2) /. 1
in rng (Line (G1,1))
by A738, PARTFUN2:2;
verum end; end; end;
rng tt c= rng f
by A351, A354;
then A740:
rng tt c= rng g1
by A178;
now for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. (len h1) = G1 * (i1,i2) & F /. 1 = G1 * (j1,j2) & len h1 in dom h1 & 1 in dom F holds
|.(i1 - j1).| + |.(i2 - j2).| = 1A741:
[mi,K1] in Indices G1
by A39, A96, A367, A400, ZFMISC_1:87;
reconsider w4 =
(pf + 1) - 1 as
Nat ;
let i1,
i2,
j1,
j2 be
Nat;
( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & h1 /. (len h1) = G1 * (i1,i2) & F /. 1 = G1 * (j1,j2) & len h1 in dom h1 & 1 in dom F implies |.(i1 - j1).| + |.(i2 - j2).| = 1 )assume that A742:
[i1,i2] in Indices G1
and A743:
[j1,j2] in Indices G1
and A744:
h1 /. (len h1) = G1 * (
i1,
i2)
and A745:
F /. 1
= G1 * (
j1,
j2)
and A746:
len h1 in dom h1
and A747:
1
in dom F
;
|.(i1 - j1).| + |.(i2 - j2).| = 1F /. 1 =
((g2 | m) | pf) /. w4
by A663, A664, A747
.=
(g2 | m) /. w4
by A654, A663, A664, A747
.=
G1 * (
mi,
K1)
by A367, A368, A400, A526, MATRIX_0:def 7
;
then A748:
(
j1 = mi &
j2 = K1 )
by A743, A745, A741, GOBOARD1:5;
l1 in dom G1
by A369, A401, A746;
then A749:
[l1,K1] in Indices G1
by A96, A367, A400, ZFMISC_1:87;
h1 /. (len h1) = G1 * (
l1,
K1)
by A369, A746;
then
(
i1 = l1 &
i2 = K1 )
by A742, A744, A749, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| =
|.((mi - 1) - mi).| + 0
by A748, ABSVALUE:2
.=
|.(- 1).|
.=
|.1.|
by COMPLEX1:52
.=
1
by ABSVALUE:def 1
;
verum end; then
for
n being
Nat st
n in dom (h1 ^ F) &
n + 1
in dom (h1 ^ F) holds
for
i1,
i2,
j1,
j2 being
Nat st
[i1,i2] in Indices G1 &
[j1,j2] in Indices G1 &
(h1 ^ F) /. n = G1 * (
i1,
i2) &
(h1 ^ F) /. (n + 1) = G1 * (
j1,
j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1
by A408, A724, GOBOARD1:24;
then
for
n being
Nat st
n in dom ((h1 ^ F) ^ h2) &
n + 1
in dom ((h1 ^ F) ^ h2) holds
for
m,
k,
i,
j being
Nat st
[m,k] in Indices G1 &
[i,j] in Indices G1 &
((h1 ^ F) ^ h2) /. n = G1 * (
m,
k) &
((h1 ^ F) ^ h2) /. (n + 1) = G1 * (
i,
j) holds
|.(m - i).| + |.(k - j).| = 1
by A475, A669, GOBOARD1:24;
then
(h1 ^ F) ^ h2 is_sequence_on G1
by A682, GOBOARD1:def 9;
then A750:
(h1 ^ F) ^ h2 is_sequence_on DelCol (
G1,
(width G1))
by A73, A152, A723, GOBOARD1:25;
A751:
len ((h1 ^ F) ^ h2) =
(len (h1 ^ F)) + (len h2)
by FINSEQ_1:22
.=
((len h1) + (len F)) + (len h2)
by FINSEQ_1:22
;
then
1
in dom ((h1 ^ F) ^ h2)
by A683, FINSEQ_3:25;
then A752:
((h1 ^ F) ^ h2) /. 1
in rng (Line ((DelCol (G1,(width G1))),1))
by A73, A26, A152, A731, A723, MATRIX_0:75;
A753:
now ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1)))per cases
( ma = len G1 or ma <> len G1 )
;
suppose A754:
ma = len G1
;
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1)))A755:
pl in Seg pf
by A487, A653, FINSEQ_1:1;
A756:
(pf + 1) - ((pf + 1) - pl) = pl
;
A757:
len F in dom F
by A663, A668, FINSEQ_3:25;
h2 = {}
by A421, A754;
then A758:
(h1 ^ F) ^ h2 = h1 ^ F
by FINSEQ_1:34;
then ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) =
((h1 ^ F) ^ h2) /. ((len h1) + (len F))
by FINSEQ_1:22
.=
F /. LL
by A663, A758, A757, FINSEQ_4:69
.=
((g2 | m) | pf) /. pl
by A663, A664, A756, A757
.=
(g2 | m) /. pl
by A359, A755, FINSEQ_4:71
;
hence
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1)))
by A363, A754;
verum end; suppose A759:
ma <> len G1
;
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1)))
ma <= len G1
by A41, FINSEQ_3:25;
then
ma < len G1
by A759, XXREAL_0:1;
then
ma + 1
<= len G1
by NAT_1:13;
then A760:
1
<= l2
by XREAL_1:19;
then A761:
l2 in Seg l2
by FINSEQ_1:1;
len (Line (G1,(len G1))) = width G1
by MATRIX_0:def 7;
then A762:
K2 in dom Ll
by A365, A355, FINSEQ_1:def 3;
then A763:
Ll /. K2 = Ll . K2
by PARTFUN1:def 6;
A764:
len h2 in dom h2
by A421, A760, FINSEQ_3:25;
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) =
((h1 ^ F) ^ h2) /. ((len (h1 ^ F)) + (len h2))
by FINSEQ_1:22
.=
h2 /. l2
by A421, A764, FINSEQ_4:69
.=
G1 * (
(ma + l2),
K2)
by A421, A485, A761
.=
Ll /. K2
by A365, A355, A763, MATRIX_0:def 7
;
hence
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1)))
by A762, PARTFUN2:2;
verum end; end; end;
len ((h1 ^ F) ^ h2) in dom ((h1 ^ F) ^ h2)
by A751, A683, FINSEQ_3:25;
then A765:
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line ((DelCol (G1,(width G1))),(len (DelCol (G1,(width G1))))))
by A73, A27, A152, A153, A753, A723, MATRIX_0:75;
width (DelCol (G1,(width G1))) = k
by A3, A73, MATRIX_0:63;
then
(rng ((h1 ^ F) ^ h2)) /\ (rng tt) <> {}
by A2, A92, A353, A751, A683, A750, A752, A765, A341;
then A766:
the
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng tt) in (rng ((h1 ^ F) ^ h2)) /\ (rng tt)
;
(rng tt) /\ (rng ((h1 ^ F) ^ h2)) =
(((rng h1) \/ (rng F)) /\ (rng tt)) \/ {}
by A492, A684, XBOOLE_1:23
.=
{} \/ ((rng F) /\ (rng tt))
by A424, XBOOLE_1:23
.=
(rng tt) /\ (rng F)
;
then
(rng ((h1 ^ F) ^ h2)) /\ (rng tt) c= (rng g1) /\ (rng g2)
by A740, A665, XBOOLE_1:27;
hence
(rng g1) /\ (rng g2) <> {}
by A766;
verum end; end; end; hence
(rng g1) /\ (rng g2) <> {}
;
verum end; end; end; hence
(rng g1) /\ (rng g2) <> {}
;
verum end; end;
end; end; end; end; hence
(rng g1) /\ (rng g2) <> {}
;
verum end; end; end;
hence
(rng g1) /\ (rng g2) <> {}
;
verum
end;
A767:
S1[ 0 ]
;
A768:
for k being Nat holds S1[k]
from NAT_1:sch 2(A767, A1);
A769:
now for k being Nat
for G1 being Go-board
for g1, g2 being FinSequence of (TOP-REAL 2) st k = width G1 & k > 0 & 1 <= len g1 & 1 <= len g2 & g1 is_sequence_on G1 & g2 is_sequence_on G1 & g1 /. 1 in rng (Line (G1,1)) & g1 /. (len g1) in rng (Line (G1,(len G1))) & g2 /. 1 in rng (Col (G1,1)) & g2 /. (len g2) in rng (Col (G1,(width G1))) holds
rng g1 meets rng g2let k be
Nat;
for G1 being Go-board
for g1, g2 being FinSequence of (TOP-REAL 2) st k = width G1 & k > 0 & 1 <= len g1 & 1 <= len g2 & g1 is_sequence_on G1 & g2 is_sequence_on G1 & g1 /. 1 in rng (Line (G1,1)) & g1 /. (len g1) in rng (Line (G1,(len G1))) & g2 /. 1 in rng (Col (G1,1)) & g2 /. (len g2) in rng (Col (G1,(width G1))) holds
rng g1 meets rng g2let G1 be
Go-board;
for g1, g2 being FinSequence of (TOP-REAL 2) st k = width G1 & k > 0 & 1 <= len g1 & 1 <= len g2 & g1 is_sequence_on G1 & g2 is_sequence_on G1 & g1 /. 1 in rng (Line (G1,1)) & g1 /. (len g1) in rng (Line (G1,(len G1))) & g2 /. 1 in rng (Col (G1,1)) & g2 /. (len g2) in rng (Col (G1,(width G1))) holds
rng g1 meets rng g2let g1,
g2 be
FinSequence of
(TOP-REAL 2);
( k = width G1 & k > 0 & 1 <= len g1 & 1 <= len g2 & g1 is_sequence_on G1 & g2 is_sequence_on G1 & g1 /. 1 in rng (Line (G1,1)) & g1 /. (len g1) in rng (Line (G1,(len G1))) & g2 /. 1 in rng (Col (G1,1)) & g2 /. (len g2) in rng (Col (G1,(width G1))) implies rng g1 meets rng g2 )assume
(
k = width G1 &
k > 0 & 1
<= len g1 & 1
<= len g2 &
g1 is_sequence_on G1 &
g2 is_sequence_on G1 &
g1 /. 1
in rng (Line (G1,1)) &
g1 /. (len g1) in rng (Line (G1,(len G1))) &
g2 /. 1
in rng (Col (G1,1)) &
g2 /. (len g2) in rng (Col (G1,(width G1))) )
;
rng g1 meets rng g2then
(rng g1) /\ (rng g2) <> {}
by A768;
hence
rng g1 meets rng g2
by XBOOLE_0:def 7;
verum end;
width G <> 0
by MATRIX_0:def 10;
then A770:
width G > 0
;
assume
( 1 <= len f1 & 1 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line (G,1)) & f1 /. (len f1) in rng (Line (G,(len G))) & f2 /. 1 in rng (Col (G,1)) & f2 /. (len f2) in rng (Col (G,(width G))) )
; rng f1 meets rng f2
hence
rng f1 meets rng f2
by A769, A770; verum