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