let G be Go-board; :: thesis: 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); :: thesis: ( 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 )
assume A1:
( 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)) )
; :: thesis: rng f1 meets rng f2
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) <> {} ;
A2:
S1[ 0 ]
;
A3:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
:: thesis: S1[k + 1]
let G1 be
Go-board;
:: thesis: 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);
:: thesis: ( 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 A5:
(
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)) )
;
:: thesis: (rng g1) /\ (rng g2) <> {}
A6:
(
dom g1 = Seg (len g1) &
dom g2 = Seg (len g2) )
by FINSEQ_1:def 3;
defpred S2[
Nat]
means ( $1
in dom g2 &
g2 /. $1
in rng (Col G1,(width G1)) );
A7:
ex
m being
Nat st
S2[
m]
consider m being
Nat such that A8:
(
S2[
m] & ( for
i being
Nat st
S2[
i] holds
m <= i ) )
from NAT_1:sch 5(A7);
reconsider m =
m as
Element of
NAT by ORDINAL1:def 13;
set g =
g2 | m;
A9:
1
<= len (g2 | m)
by A8, GOBOARD1:38;
A10:
g2 | m is_sequence_on G1
by A5, GOBOARD1:38;
A11:
(g2 | m) /. 1
in rng (Col G1,1)
by A5, A8, GOBOARD1:22;
A12:
(g2 | m) /. (len (g2 | m)) in rng (Col G1,(width G1))
by A8, GOBOARD1:23;
(
0 <> width G1 &
0 <> len G1 )
by GOBOARD1:def 5;
then A13:
(
0 + 1
<= width G1 &
0 + 1
<= len G1 )
by NAT_1:14;
then A14:
1
in Seg (width G1)
by FINSEQ_1:3;
A15:
width G1 in Seg (width G1)
by A13, FINSEQ_1:3;
A16:
1
in dom G1
by A13, FINSEQ_3:27;
A17:
len G1 in dom G1
by A13, FINSEQ_3:27;
A18:
1
in dom (g2 | m)
by A9, FINSEQ_3:27;
A19:
dom (g2 | m) = Seg (len (g2 | m))
by FINSEQ_1:def 3;
reconsider L1 =
Line G1,1,
Ll =
Line G1,
(len G1) as
FinSequence of
(TOP-REAL 2) ;
defpred S3[
Nat]
means ( $1
in dom G1 &
(rng (g2 | m)) /\ (rng (Line G1,$1)) <> {} );
A20:
ex
n being
Nat st
S3[
n]
proof
consider i being
Nat such that A21:
(
i in dom (Col G1,1) &
(g2 | m) /. 1
= (Col G1,1) . i )
by A11, FINSEQ_2:11;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 13;
A22:
i in Seg (len (Col G1,1))
by A21, FINSEQ_1:def 3;
take
i
;
:: thesis: S3[i]
(
len (Col G1,1) = len G1 &
len (Line G1,i) = width G1 )
by MATRIX_1:def 8, MATRIX_1:def 9;
then A23:
dom (Line G1,i) = Seg (width G1)
by FINSEQ_1:def 3;
i in Seg (len G1)
by A22, MATRIX_1:def 9;
hence
i in dom G1
by FINSEQ_1:def 3;
:: thesis: (rng (g2 | m)) /\ (rng (Line G1,i)) <> {}
then
(g2 | m) /. 1
= (Line G1,i) . 1
by A14, A21, GOBOARD1:17;
then
(
(g2 | m) /. 1
in rng (Line G1,i) &
(g2 | m) /. 1
in rng (g2 | m) )
by A14, A18, A23, FUNCT_1:def 5, PARTFUN2:4;
hence
(rng (g2 | m)) /\ (rng (Line G1,i)) <> {}
by XBOOLE_0:def 4;
:: thesis: verum
end;
then A24:
ex
n being
Nat st
S3[
n]
;
A25:
for
n being
Nat st
S3[
n] holds
n <= len G1
by FINSEQ_3:27;
consider mi being
Nat such that A26:
(
S3[
mi] & ( for
n being
Nat st
S3[
n] holds
mi <= n ) )
from NAT_1:sch 5(A20);
A27:
dom G1 = Seg (len G1)
by FINSEQ_1:def 3;
consider ma being
Nat such that A28:
(
S3[
ma] & ( for
n being
Nat st
S3[
n] holds
n <= ma ) )
from NAT_1:sch 6(A25, A24);
reconsider mi =
mi,
ma =
ma as
Element of
NAT by ORDINAL1:def 13;
defpred S4[
Nat]
means ( $1
in dom g1 &
g1 /. $1
in rng (Line G1,mi) );
A29:
( 1
<= mi &
mi <= len G1 &
ma <= len G1 )
by A26, A28, FINSEQ_3:27;
then
ex
n being
Element of
NAT st
S4[
n]
by A5, GOBOARD1:45;
then A30:
ex
n being
Nat st
S4[
n]
;
A31:
for
n being
Nat st
S4[
n] holds
n <= len g1
by FINSEQ_3:27;
consider ma1 being
Nat such that A32:
(
S4[
ma1] & ( for
n being
Nat st
S4[
n] holds
n <= ma1 ) )
from NAT_1:sch 6(A31, A30);
A33:
for
n being
Element of
NAT st
S4[
n] holds
n <= ma1
by A32;
reconsider ma1 =
ma1 as
Element of
NAT by ORDINAL1:def 13;
A34:
( 1
<= m &
m <= len g2 )
by A8, FINSEQ_3:27;
then A35:
len (g2 | m) = m
by FINSEQ_1:80;
A36:
rng (g2 | m) c= rng g2
reconsider Lmi =
Line G1,
mi as
FinSequence of
(TOP-REAL 2) ;
A38:
(
mi = ma implies
(rng g1) /\ (rng g2) <> {} )
proof
assume A39:
mi = ma
;
:: thesis: (rng g1) /\ (rng g2) <> {}
consider n being
Element of
NAT such that A40:
(
n in dom g1 &
g1 /. n in rng (Line G1,mi) )
by A5, A29, GOBOARD1:45;
consider i being
Element of
NAT such that A41:
(
i in dom (Line G1,mi) &
g1 /. n = Lmi /. i )
by A40, PARTFUN2:4;
A42:
dom (Line G1,mi) = Seg (len (Line G1,mi))
by FINSEQ_1:def 3;
reconsider Ci =
Col G1,
i as
FinSequence of
(TOP-REAL 2) ;
A43:
(
len (Line G1,mi) = width G1 &
len (Col G1,i) = len G1 )
by MATRIX_1:def 8, MATRIX_1:def 9;
then
( 1
<= i &
i <= width G1 )
by A41, FINSEQ_3:27;
then consider m being
Element of
NAT such that A44:
(
m in dom (g2 | m) &
(g2 | m) /. m in rng (Col G1,i) )
by A9, A10, A11, A12, GOBOARD1:49;
A45:
dom (Col G1,i) =
Seg (len G1)
by A43, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
consider j being
Element of
NAT such that A46:
(
j in dom Ci &
(g2 | m) /. m = Ci /. j )
by A44, PARTFUN2:4;
A47:
dom Ci = Seg (len Ci)
by FINSEQ_1:def 3;
reconsider Lj =
Line G1,
j as
FinSequence of
(TOP-REAL 2) ;
A48:
(g2 | m) /. m in rng (g2 | m)
by A44, PARTFUN2:4;
A49:
g1 /. n in rng g1
by A40, PARTFUN2:4;
len (Line G1,mi) =
width G1
by MATRIX_1:def 8
.=
len Lj
by MATRIX_1:def 8
;
then A50:
dom (Line G1,mi) = dom Lj
by A42, FINSEQ_1:def 3;
A51:
(g2 | m) /. m =
Ci . j
by A46, PARTFUN1:def 8
.=
Lj . i
by A41, A42, A43, A45, A46, GOBOARD1:17
.=
Lj /. i
by A41, A50, PARTFUN1:def 8
;
len Lj = width G1
by MATRIX_1:def 8;
then
i in dom Lj
by A41, A42, A43, FINSEQ_1:def 3;
then
(g2 | m) /. m in rng Lj
by A51, PARTFUN2:4;
then A52:
(rng (g2 | m)) /\ (rng (Line G1,j)) <> {}
by A48, XBOOLE_0:def 4;
hence
(rng g1) /\ (rng g2) <> {}
by A36, A41, A48, A49, A51, XBOOLE_0:def 4;
:: thesis: verum
end;
consider k1 being
Element of
NAT such that A53:
(
k1 in dom Lmi &
g1 /. ma1 = Lmi /. k1 )
by A32, PARTFUN2:4;
A54:
Seg (len Lmi) = dom Lmi
by FINSEQ_1:def 3;
reconsider Ck1 =
Col G1,
k1 as
FinSequence of
(TOP-REAL 2) ;
( 1
<= mi &
ma <= len G1 )
by A26, A28, FINSEQ_3:27;
then reconsider l1 =
mi - 1,
l2 =
(len G1) - ma as
Element of
NAT by INT_1:18;
deffunc H1(
Nat)
-> Element of the
carrier of
(TOP-REAL 2) =
G1 * $1,
k1;
consider h1 being
FinSequence of
(TOP-REAL 2) such that A55:
(
len h1 = l1 & ( for
n being
Nat st
n in dom h1 holds
h1 /. n = H1(
n) ) )
from FINSEQ_4:sch 2();
A56:
k1 in Seg (width G1)
by A53, A54, MATRIX_1:def 8;
now per cases
( k = 0 or k <> 0 )
;
suppose A57:
k = 0
;
:: thesis: (rng g1) /\ (rng g2) <> {} reconsider c1 =
Col G1,1 as
FinSequence of
(TOP-REAL 2) ;
consider x being
Element of
NAT such that A58:
(
x in dom c1 &
g2 /. 1
= c1 /. x )
by A5, PARTFUN2:4;
A59:
(
Seg (len c1) = dom c1 &
dom c1 c= NAT &
len c1 = len G1 &
dom G1 = Seg (len G1) )
by FINSEQ_1:def 3, MATRIX_1:def 9;
reconsider lx =
Line G1,
x as
FinSequence of
(TOP-REAL 2) ;
0 <> width G1
by GOBOARD1:def 5;
then
0 + 1
<= width G1
by NAT_1:14;
then A60:
( 1
in Seg (width G1) &
x in dom G1 &
Seg (len lx) = dom lx &
len lx = width G1 &
Seg (len g2) = dom g2 )
by A58, A59, FINSEQ_1:3, FINSEQ_1:def 3, MATRIX_1:def 8;
( 1
<= x &
x <= len G1 )
by A58, A59, FINSEQ_3:27;
then consider m being
Element of
NAT such that A61:
(
m in dom g1 &
g1 /. m in rng lx )
by A5, GOBOARD1:45;
consider y being
Element of
NAT such that A62:
(
y in dom lx &
lx /. y = g1 /. m )
by A61, PARTFUN2:4;
A63:
(
lx /. y = lx . y &
c1 /. x = c1 . x )
by A58, A62, PARTFUN1:def 8;
A64:
(
y = 1 & 1
in dom g2 )
by A5, A57, A60, A62, FINSEQ_1:4, FINSEQ_3:27, TARSKI:def 1;
then A65:
g1 /. m = g2 /. 1
by A58, A60, A62, A63, GOBOARD1:17;
A66:
g1 /. m in rng g1
by A61, PARTFUN2:4;
g2 /. 1
in rng g2
by A64, PARTFUN2:4;
hence
(rng g1) /\ (rng g2) <> {}
by A65, A66, XBOOLE_0:def 4;
:: thesis: verum end; suppose A67:
k <> 0
;
:: thesis: (rng g1) /\ (rng g2) <> {} then A68:
0 < k
by NAT_1:3;
now per cases
( mi = ma or mi <> ma )
;
suppose A69:
mi <> ma
;
:: thesis: (rng g1) /\ (rng g2) <> {} defpred S5[
Nat]
means ( $1
in dom g1 &
ma1 < $1 &
g1 /. $1
in rng (Line G1,ma) );
A70:
mi <= ma
by A26, A28;
then A71:
mi < ma
by A69, XXREAL_0:1;
then
ex
n being
Element of
NAT st
S5[
n]
by A5, A26, A29, A32, GOBOARD1:53;
then A72:
ex
n being
Nat st
S5[
n]
;
consider mi1 being
Nat such that A73:
(
S5[
mi1] & ( for
n being
Nat st
S5[
n] holds
mi1 <= n ) )
from NAT_1:sch 5(A72);
set f1 =
g1 | mi1;
(
ma1 <= mi1 &
mi1 <= mi1 + 1 )
by A73, NAT_1:11;
then reconsider l =
(mi1 + 1) - ma1 as
Element of
NAT by INT_1:18, XXREAL_0:2;
1
<= ma1
by A32, FINSEQ_3:27;
then reconsider w =
ma1 - 1 as
Element of
NAT by INT_1:18;
A74:
for
n being
Element of
NAT st
n in Seg l holds
(
(g1 | mi1) /. (w + n) = g1 /. (w + n) &
w + n in dom g1 )
defpred S6[
Nat,
Element of
(TOP-REAL 2)]
means $2
= (g1 | mi1) /. (w + $1);
A77:
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 A78:
(
len f = l & ( for
n being
Nat st
n in Seg l holds
S6[
n,
f /. n] ) )
from FINSEQ_4:sch 1(A77);
A79:
dom f = Seg l
by A78, FINSEQ_1:def 3;
reconsider Lma =
Line G1,
ma as
FinSequence of
(TOP-REAL 2) ;
consider k2 being
Element of
NAT such that A80:
(
k2 in dom Lma &
g1 /. mi1 = Lma /. k2 )
by A73, PARTFUN2:4;
A81:
dom Lma = Seg (len Lma)
by FINSEQ_1:def 3;
reconsider Ck2 =
Col G1,
k2 as
FinSequence of
(TOP-REAL 2) ;
A82:
k2 in Seg (width G1)
by A80, A81, MATRIX_1:def 8;
deffunc H2(
Nat)
-> Element of the
carrier of
(TOP-REAL 2) =
G1 * (ma + $1),
k2;
consider h2 being
FinSequence of
(TOP-REAL 2) such that A83:
(
len h2 = l2 & ( for
n being
Nat st
n in dom h2 holds
h2 /. n = H2(
n) ) )
from FINSEQ_4:sch 2();
A84:
dom h2 = Seg (len h2)
by FINSEQ_1:def 3;
set ff =
(h1 ^ f) ^ h2;
(
ma1 + 1
<= mi1 &
mi1 <= mi1 + 1 )
by A73, NAT_1:13;
then A85:
(
ma1 + 1
<= mi1 + 1 &
Seg (len f) = dom f &
Seg (len h2) = dom h2 &
dom h1 = Seg (len h1) )
by FINSEQ_1:def 3, XXREAL_0:2;
then A86:
( 1
<= l &
len f = l )
by A78, XREAL_1:21;
A87:
Indices G1 = [:(dom G1),(Seg (width G1)):]
by MATRIX_1:def 5;
A91:
now let n be
Element of
NAT ;
:: thesis: ( n in dom h1 implies ex i, k1 being Element of NAT st
( [i,k1] in Indices G1 & h1 /. n = G1 * i,k1 ) )assume
n in dom h1
;
:: thesis: ex i, k1 being Element of NAT st
( [i,k1] in Indices G1 & h1 /. n = G1 * i,k1 )then A92:
(
h1 /. n = G1 * n,
k1 &
n in dom G1 )
by A55, A88;
take i =
n;
:: thesis: ex k1 being Element of NAT st
( [i,k1] in Indices G1 & h1 /. n = G1 * i,k1 )take k1 =
k1;
:: thesis: ( [i,k1] in Indices G1 & h1 /. n = G1 * i,k1 )thus
(
[i,k1] in Indices G1 &
h1 /. n = G1 * i,
k1 )
by A56, A87, A92, ZFMISC_1:106;
:: thesis: verum end; A93:
now let n be
Element of
NAT ;
:: thesis: ( 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
n in dom h2
;
:: thesis: ex m being Element of NAT ex k2 being Element of NAT st
( [m,k2] in Indices G1 & h2 /. n = G1 * m,k2 )then A94:
(
h2 /. n = G1 * (ma + n),
k2 &
ma + n in dom G1 )
by A83, A90;
take m =
ma + n;
:: thesis: ex k2 being Element of NAT st
( [m,k2] in Indices G1 & h2 /. n = G1 * m,k2 )take k2 =
k2;
:: thesis: ( [m,k2] in Indices G1 & h2 /. n = G1 * m,k2 )thus
(
[m,k2] in Indices G1 &
h2 /. n = G1 * m,
k2 )
by A82, A87, A94, ZFMISC_1:106;
:: thesis: verum end; A95:
now let n be
Element of
NAT ;
:: thesis: ( n in dom f implies ex i, j being Element of NAT st
( [i,j] in Indices G1 & f /. n = G1 * i,j ) )assume
n in dom f
;
:: thesis: ex i, j being Element of NAT st
( [i,j] in Indices G1 & f /. n = G1 * i,j )then A96:
(
n in Seg l &
dom f = Seg l &
f /. n = (g1 | mi1) /. (w + n) )
by A78, A79;
then
(
w is
Element of
NAT &
w + n in dom g1 &
f /. n = g1 /. (w + n) )
by A74;
then consider i,
j being
Element of
NAT such that A97:
(
[i,j] in Indices G1 &
g1 /. (w + n) = G1 * i,
j )
by A5, GOBOARD1:def 11;
take i =
i;
:: thesis: ex j being Element of NAT st
( [i,j] in Indices G1 & f /. n = G1 * i,j )take j =
j;
:: thesis: ( [i,j] in Indices G1 & f /. n = G1 * i,j )thus
(
[i,j] in Indices G1 &
f /. n = G1 * i,
j )
by A74, A96, A97;
:: thesis: 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 A91, GOBOARD1:39;
then A98:
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 A93, GOBOARD1:39;
A99:
now let n be
Element of
NAT ;
:: thesis: ( 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
(
n in dom h1 &
n + 1
in dom h1 )
;
:: thesis: 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)) = 1then A100:
(
n in dom G1 &
n + 1
in dom G1 &
h1 /. n = G1 * n,
k1 &
h1 /. (n + 1) = G1 * (n + 1),
k1 )
by A55, A88;
then A101:
(
[n,k1] in Indices G1 &
[(n + 1),k1] in Indices G1 )
by A56, A87, ZFMISC_1:106;
let i1,
i2,
j1,
j2 be
Element of
NAT ;
:: thesis: ( [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
(
[i1,i2] in Indices G1 &
[j1,j2] in Indices G1 &
h1 /. n = G1 * i1,
i2 &
h1 /. (n + 1) = G1 * j1,
j2 )
;
:: thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1then
(
i1 = n &
i2 = k1 &
j1 = n + 1 &
j2 = k1 &
0 <= 1 )
by A100, A101, GOBOARD1:21;
hence (abs (i1 - j1)) + (abs (i2 - j2)) =
(abs ((n - n) + (- 1))) + 0
by ABSVALUE:7
.=
abs 1
by COMPLEX1:138
.=
1
by ABSVALUE:def 1
;
:: thesis: verum end; A102:
w + l = mi1
;
A103:
now let n be
Element of
NAT ;
:: thesis: ( 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
(
n in dom h2 &
n + 1
in dom h2 )
;
:: thesis: 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)) = 1then A104:
(
ma + n in dom G1 &
ma + (n + 1) in dom G1 &
h2 /. n = G1 * (ma + n),
k2 &
h2 /. (n + 1) = G1 * (ma + (n + 1)),
k2 &
ma + (n + 1) = (ma + n) + 1 )
by A83, A90;
then A105:
(
[(ma + n),k2] in Indices G1 &
[((ma + n) + 1),k2] in Indices G1 )
by A82, A87, ZFMISC_1:106;
let i1,
i2,
j1,
j2 be
Element of
NAT ;
:: thesis: ( [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
(
[i1,i2] in Indices G1 &
[j1,j2] in Indices G1 &
h2 /. n = G1 * i1,
i2 &
h2 /. (n + 1) = G1 * j1,
j2 )
;
:: thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1then
(
i1 = ma + n &
i2 = k2 &
j1 = (ma + n) + 1 &
j2 = k2 &
0 <= 1 )
by A104, A105, GOBOARD1:21;
hence (abs (i1 - j1)) + (abs (i2 - j2)) =
(abs (((ma + n) - (ma + n)) + (- 1))) + 0
by ABSVALUE:7
.=
abs 1
by COMPLEX1:138
.=
1
by ABSVALUE:def 1
;
:: thesis: verum end; A106:
now let n be
Element of
NAT ;
:: thesis: ( 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
(
n in dom f &
n + 1
in dom f )
;
:: thesis: 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)) = 1then
(
n in Seg l &
n + 1
in Seg l &
dom f = Seg l &
f /. n = (g1 | mi1) /. (w + n) &
f /. (n + 1) = (g1 | mi1) /. (w + (n + 1)) &
w + (n + 1) = (w + n) + 1 )
by A78, A79;
then A107:
(
w is
Element of
NAT &
w + n in dom g1 &
f /. n = g1 /. (w + n) &
(w + n) + 1
in dom g1 &
f /. (n + 1) = g1 /. ((w + n) + 1) )
by A74;
let i1,
i2,
j1,
j2 be
Element of
NAT ;
:: thesis: ( [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
(
[i1,i2] in Indices G1 &
[j1,j2] in Indices G1 &
f /. n = G1 * i1,
i2 &
f /. (n + 1) = G1 * j1,
j2 )
;
:: thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1hence
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
by A5, A107, GOBOARD1:def 11;
:: thesis: verum end; now let i1,
i2,
j1,
j2 be
Element of
NAT ;
:: thesis: ( [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 A108:
(
[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 )
;
:: thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1then A109:
(
h1 /. (len h1) = G1 * l1,
k1 &
l1 in dom G1 )
by A55, A88;
then
[l1,k1] in Indices G1
by A56, A87, ZFMISC_1:106;
then A110:
(
i1 = l1 &
i2 = k1 &
0 <= 1 )
by A108, A109, GOBOARD1:21;
A111:
Lmi /. k1 = Lmi . k1
by A53, PARTFUN1:def 8;
A112:
w + 1
= ma1
;
then
( 1
in Seg l &
dom f = Seg l &
f /. 1
= (g1 | mi1) /. ma1 )
by A78, A79, A108;
then A113:
f /. 1 =
g1 /. ma1
by A74, A112
.=
G1 * mi,
k1
by A53, A56, A111, MATRIX_1:def 8
;
[mi,k1] in Indices G1
by A26, A56, A87, ZFMISC_1:106;
then
(
j1 = mi &
j2 = k1 )
by A108, A113, GOBOARD1:21;
hence (abs (i1 - j1)) + (abs (i2 - j2)) =
(abs ((mi - 1) - mi)) + 0
by A110, ABSVALUE:7
.=
abs (- 1)
.=
abs 1
by COMPLEX1:138
.=
1
by ABSVALUE:def 1
;
:: thesis: verum end; then A114:
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 A99, A106, GOBOARD1:40;
set hf =
h1 ^ f;
now let i1,
i2,
j1,
j2 be
Element of
NAT ;
:: thesis: ( [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 A115:
(
[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 )
;
:: thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1then A116:
(
h2 /. 1
= G1 * (ma + 1),
k2 &
ma + 1
in dom G1 )
by A83, A90;
then
[(ma + 1),k2] in Indices G1
by A82, A87, ZFMISC_1:106;
then A117:
(
j1 = ma + 1 &
j2 = k2 )
by A115, A116, GOBOARD1:21;
A118:
(
len f in dom f &
0 <= 1 )
by A79, A86, FINSEQ_1:3;
A119:
Lma /. k2 = Lma . k2
by A80, PARTFUN1:def 8;
A120:
(h1 ^ f) /. (len (h1 ^ f)) =
(h1 ^ f) /. ((len h1) + (len f))
by FINSEQ_1:35
.=
f /. (len f)
by A118, FINSEQ_4:84
.=
(g1 | mi1) /. (w + l)
by A78, A79, A118
.=
g1 /. mi1
by A74, A78, A79, A118
.=
G1 * ma,
k2
by A80, A82, A119, MATRIX_1:def 8
;
[ma,k2] in Indices G1
by A28, A82, A87, ZFMISC_1:106;
then
(
i1 = ma &
i2 = k2 )
by A115, A120, GOBOARD1:21;
hence (abs (i1 - j1)) + (abs (i2 - j2)) =
(abs (ma - (ma + 1))) + 0
by A117, ABSVALUE:7
.=
abs (- ((ma + 1) - ma))
.=
abs 1
by COMPLEX1:138
.=
1
by ABSVALUE:def 1
;
:: thesis: verum end; 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 A103, A114, GOBOARD1:40;
then A121:
(h1 ^ f) ^ h2 is_sequence_on G1
by A98, GOBOARD1:def 11;
A122:
now per cases
( mi = 1 or mi <> 1 )
;
suppose A123:
mi = 1
;
:: thesis: ((h1 ^ f) ^ h2) /. 1 in rng (Line G1,1)then
h1 = {}
by A55;
then A124:
(h1 ^ f) ^ h2 = f ^ h2
by FINSEQ_1:47;
A125:
( 1
in Seg l & 1
<= ma1 )
by A6, A32, A86, FINSEQ_1:3;
then A126:
ma1 in Seg mi1
by A73, FINSEQ_1:3;
A127:
w + 1
= ma1
;
((h1 ^ f) ^ h2) /. 1 =
f /. 1
by A79, A124, A125, FINSEQ_4:83
.=
(g1 | mi1) /. ma1
by A78, A125, A127
.=
g1 /. ma1
by A73, A126, FINSEQ_4:86
;
hence
((h1 ^ f) ^ h2) /. 1
in rng (Line G1,1)
by A32, A123;
:: thesis: verum end; suppose A128:
mi <> 1
;
:: thesis: ((h1 ^ f) ^ h2) /. 1 in rng (Line G1,1)
1
<= mi
by A26, FINSEQ_3:27;
then
1
< mi
by A128, XXREAL_0:1;
then
1
+ 1
<= mi
by NAT_1:13;
then A129:
1
<= l1
by XREAL_1:21;
then A130:
1
in dom h1
by A55, FINSEQ_3:27;
A131:
len (h1 ^ f) = (len h1) + (len f)
by FINSEQ_1:35;
A132:
len (Line G1,1) = width G1
by MATRIX_1:def 8;
then
dom (Line G1,1) = Seg (width G1)
by FINSEQ_1:def 3;
then A133:
L1 /. k1 = L1 . k1
by A56, PARTFUN1:def 8;
0 <= len f
by NAT_1:2;
then
0 + 1
<= len (h1 ^ f)
by A55, A129, A131, XREAL_1:9;
then
1
in dom (h1 ^ f)
by FINSEQ_3:27;
then A134:
((h1 ^ f) ^ h2) /. 1 =
(h1 ^ f) /. 1
by FINSEQ_4:83
.=
h1 /. 1
by A130, FINSEQ_4:83
.=
G1 * 1,
k1
by A55, A130
.=
L1 /. k1
by A56, A133, MATRIX_1:def 8
;
k1 in dom L1
by A56, A132, FINSEQ_1:def 3;
hence
((h1 ^ f) ^ h2) /. 1
in rng (Line G1,1)
by A134, PARTFUN2:4;
:: thesis: verum A135:
len ((h1 ^ f) ^ h2) =
(len (h1 ^ f)) + (len h2)
by FINSEQ_1:35
.=
((len h1) + (len f)) + (len h2)
by FINSEQ_1:35
;
0 + 0 <= (len h1) + (len h2)
by NAT_1:2;
then A136:
0 + 1
<= (len f) + ((len h1) + (len h2))
by A86, XREAL_1:9;
A137:
now per cases
( ma = len G1 or ma <> len G1 )
;
suppose A138:
ma = len G1
;
:: thesis: ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line G1,(len G1))then
h2 = {}
by A83;
then A139:
(
(h1 ^ f) ^ h2 = h1 ^ f & 1
<= mi1 )
by A73, FINSEQ_1:47, FINSEQ_3:27;
then A140:
(
len f in dom f &
mi1 in Seg mi1 )
by A85, A86, FINSEQ_1:3;
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) =
((h1 ^ f) ^ h2) /. ((len h1) + (len f))
by A139, FINSEQ_1:35
.=
f /. l
by A78, A139, A140, FINSEQ_4:84
.=
(g1 | mi1) /. mi1
by A78, A79, A102, A140
.=
g1 /. mi1
by A73, A140, FINSEQ_4:86
;
hence
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line G1,(len G1))
by A73, A138;
:: thesis: verum end; suppose A141:
ma <> len G1
;
:: thesis: ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line G1,(len G1))
ma <= len G1
by A28, FINSEQ_3:27;
then
ma < len G1
by A141, XXREAL_0:1;
then
ma + 1
<= len G1
by NAT_1:13;
then A142:
1
<= l2
by XREAL_1:21;
then A143:
l2 in Seg l2
by FINSEQ_1:3;
A144:
len h2 in dom h2
by A83, A142, FINSEQ_3:27;
A145:
len (Line G1,(len G1)) = width G1
by MATRIX_1:def 8;
then
k2 in dom Ll
by A82, FINSEQ_1:def 3;
then A146:
Ll /. k2 = Ll . k2
by PARTFUN1:def 8;
A147:
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) =
((h1 ^ f) ^ h2) /. ((len (h1 ^ f)) + (len h2))
by FINSEQ_1:35
.=
h2 /. l2
by A83, A144, FINSEQ_4:84
.=
G1 * (ma + l2),
k2
by A83, A84, A143
.=
Ll /. k2
by A82, A146, MATRIX_1:def 8
;
k2 in dom Ll
by A82, A145, FINSEQ_1:def 3;
hence
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line G1,(len G1))
by A147, PARTFUN2:4;
:: thesis: verum end; A148:
rng ((h1 ^ f) ^ h2) =
(rng (h1 ^ f)) \/ (rng h2)
by FINSEQ_1:44
.=
((rng h1) \/ (rng f)) \/ (rng h2)
by FINSEQ_1:44
;
A149:
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
let k be
Element of
NAT ;
:: thesis: ( k in Seg (width G1) & (rng f) /\ (rng (Col G1,k)) = {} implies (rng ((h1 ^ f) ^ h2)) /\ (rng (Col G1,k)) = {} )
assume that A150:
k in Seg (width G1)
and A151:
(rng f) /\ (rng (Col G1,k)) = {}
;
:: thesis: (rng ((h1 ^ f) ^ h2)) /\ (rng (Col G1,k)) = {}
set gg =
Col G1,
k;
assume A152:
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col G1,k)) <> {}
;
:: thesis: contradiction
consider x being
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col G1,k));
A153:
w + 1
= ma1
;
rng ((h1 ^ f) ^ h2) = (rng f) \/ ((rng h1) \/ (rng h2))
by A148, XBOOLE_1:4;
then A154:
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col G1,k)) =
{} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col G1,k)))
by A151, XBOOLE_1:23
.=
((rng h1) /\ (rng (Col G1,k))) \/ ((rng h2) /\ (rng (Col G1,k)))
by XBOOLE_1:23
;
A155:
(
len (Col G1,k1) = len G1 &
len (Col G1,k2) = len G1 )
by MATRIX_1:def 9;
now per cases
( x in (rng h1) /\ (rng (Col G1,k)) or x in (rng h2) /\ (rng (Col G1,k)) )
by A152, A154, XBOOLE_0:def 3;
suppose
x in (rng h1) /\ (rng (Col G1,k))
;
:: thesis: contradictionthen A156:
(
x in rng h1 &
x in rng (Col G1,k) )
by XBOOLE_0:def 4;
then consider i being
Element of
NAT such that A157:
(
i in dom h1 &
x = h1 /. i )
by PARTFUN2:4;
A158:
x = G1 * i,
k1
by A55, A157;
reconsider y =
x as
Point of
(TOP-REAL 2) by A157;
A159:
dom (Col G1,k1) =
Seg (len G1)
by A155, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
then A160:
i in dom Ck1
by A88, A157;
A161:
(
Lmi /. k1 = Lmi . k1 &
Ck1 /. mi = Ck1 . mi )
by A26, A53, A159, PARTFUN1:def 8;
Ck1 /. i = Ck1 . i
by A88, A157, A159, PARTFUN1:def 8;
then
y = Ck1 /. i
by A158, A159, A160, MATRIX_1:def 9;
then
y in rng Ck1
by A160, PARTFUN2:4;
then A162:
(
k1 = k & 1
in Seg l )
by A56, A86, A150, A156, FINSEQ_1:3, GOBOARD1:20;
then
(
f /. 1
= (g1 | mi1) /. ma1 &
(g1 | mi1) /. ma1 = g1 /. (w + 1) )
by A74, A78, A153;
then
f /. 1
= Ck1 /. mi
by A26, A53, A56, A161, GOBOARD1:17;
then
(
f /. 1
in rng (Col G1,k) &
f /. 1
in rng f )
by A26, A79, A159, A162, PARTFUN2:4;
hence
contradiction
by A151, XBOOLE_0:def 4;
:: thesis: verum end; suppose
x in (rng h2) /\ (rng (Col G1,k))
;
:: thesis: contradictionthen A163:
(
x in rng h2 &
x in rng (Col G1,k) )
by XBOOLE_0:def 4;
then consider i being
Element of
NAT such that A164:
(
i in dom h2 &
x = h2 /. i )
by PARTFUN2:4;
A165:
x = G1 * (ma + i),
k2
by A83, A164;
reconsider y =
x as
Point of
(TOP-REAL 2) by A164;
A166:
dom (Col G1,k2) =
Seg (len G1)
by A155, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
then A167:
ma + i in dom Ck2
by A90, A164;
A168:
(
Lma /. k2 = Lma . k2 &
Ck2 /. ma = Ck2 . ma )
by A28, A80, A166, PARTFUN1:def 8;
Ck2 /. (ma + i) = Ck2 . (ma + i)
by A90, A164, A166, PARTFUN1:def 8;
then
y = Ck2 /. (ma + i)
by A165, A166, A167, MATRIX_1:def 9;
then
y in rng Ck2
by A167, PARTFUN2:4;
then A169:
(
k2 = k &
l in Seg l )
by A82, A86, A150, A163, FINSEQ_1:3, GOBOARD1:20;
then
(
f /. l = (g1 | mi1) /. (w + l) &
(g1 | mi1) /. (w + l) = g1 /. (w + l) )
by A74, A78;
then
f /. l = Ck2 /. ma
by A28, A80, A82, A168, GOBOARD1:17;
then
(
f /. l in rng (Col G1,k) &
f /. l in rng f )
by A28, A79, A166, A169, PARTFUN2:4;
hence
contradiction
by A151, XBOOLE_0:def 4;
:: thesis: verum end;
hence
contradiction
;
:: thesis: verum
end; A170:
(rng h1) /\ (rng (g2 | m)) = {}
proof
assume A171:
not
(rng h1) /\ (rng (g2 | m)) = {}
;
:: thesis: contradiction
consider x being
Element of
(rng h1) /\ (rng (g2 | m));
A172:
(
x in rng h1 &
x in rng (g2 | m) )
by A171, XBOOLE_0:def 4;
then consider n1 being
Element of
NAT such that A173:
(
n1 in dom h1 &
x = h1 /. n1 )
by PARTFUN2:4;
A174:
(
x = G1 * n1,
k1 & 1
<= n1 &
n1 <= l1 )
by A55, A173, FINSEQ_3:27;
consider n2 being
Element of
NAT such that A175:
(
n2 in dom (g2 | m) &
x = (g2 | m) /. n2 )
by A172, PARTFUN2:4;
consider i1,
i2 being
Element of
NAT such that A176:
(
[i1,i2] in Indices G1 &
(g2 | m) /. n2 = G1 * i1,
i2 )
by A10, A175, GOBOARD1:def 11;
reconsider L =
Line G1,
i1 as
FinSequence of
(TOP-REAL 2) ;
A177:
Seg (len L) = dom L
by FINSEQ_1:def 3;
A178:
(
i1 in dom G1 &
i2 in Seg (width G1) )
by A87, A176, ZFMISC_1:106;
A179:
len L = width G1
by MATRIX_1:def 8;
then
L /. i2 = L . i2
by A177, A178, PARTFUN1:def 8;
then
(g2 | m) /. n2 = L /. i2
by A176, A178, MATRIX_1:def 8;
then
(
(g2 | m) /. n2 in rng L &
(g2 | m) /. n2 in rng (g2 | m) )
by A175, A177, A178, A179, PARTFUN2:4;
then
(rng (g2 | m)) /\ (rng L) <> {}
by XBOOLE_0:def 4;
then A180:
mi <= i1
by A26, A178;
n1 in dom G1
by A88, A173;
then
[n1,k1] in Indices G1
by A56, A87, ZFMISC_1:106;
then
(
i1 = n1 &
0 < 1 )
by A174, A175, A176, GOBOARD1:21;
then
(
mi <= mi - 1 &
mi - 1
< mi )
by A174, A180, XREAL_1:46, XXREAL_0:2;
hence
contradiction
;
:: thesis: verum
end;
(rng h2) /\ (rng (g2 | m)) = {}
proof
assume A181:
not
(rng h2) /\ (rng (g2 | m)) = {}
;
:: thesis: contradiction
consider x being
Element of
(rng h2) /\ (rng (g2 | m));
A182:
(
x in rng h2 &
x in rng (g2 | m) )
by A181, XBOOLE_0:def 4;
then consider n1 being
Element of
NAT such that A183:
(
n1 in dom h2 &
x = h2 /. n1 )
by PARTFUN2:4;
A184:
(
x = G1 * (ma + n1),
k2 & 1
<= n1 &
n1 <= l2 )
by A83, A183, FINSEQ_3:27;
consider n2 being
Element of
NAT such that A185:
(
n2 in dom (g2 | m) &
x = (g2 | m) /. n2 )
by A182, PARTFUN2:4;
consider i1,
i2 being
Element of
NAT such that A186:
(
[i1,i2] in Indices G1 &
(g2 | m) /. n2 = G1 * i1,
i2 )
by A10, A185, GOBOARD1:def 11;
reconsider L =
Line G1,
i1 as
FinSequence of
(TOP-REAL 2) ;
A187:
Seg (len L) = dom L
by FINSEQ_1:def 3;
A188:
(
i1 in dom G1 &
i2 in Seg (width G1) )
by A87, A186, ZFMISC_1:106;
A189:
len L = width G1
by MATRIX_1:def 8;
then
L /. i2 = L . i2
by A187, A188, PARTFUN1:def 8;
then
(g2 | m) /. n2 = L /. i2
by A186, A188, MATRIX_1:def 8;
then
(
(g2 | m) /. n2 in rng L &
(g2 | m) /. n2 in rng (g2 | m) )
by A185, A187, A188, A189, PARTFUN2:4;
then
(rng (g2 | m)) /\ (rng L) <> {}
by XBOOLE_0:def 4;
then A190:
i1 <= ma
by A28, A188;
ma + n1 in dom G1
by A90, A183;
then
[(ma + n1),k2] in Indices G1
by A82, A87, ZFMISC_1:106;
then
i1 = ma + n1
by A184, A185, A186, GOBOARD1:21;
then
n1 <= 0
by A190, XREAL_1:31;
hence
contradiction
by A184, XXREAL_0:2;
:: thesis: verum
end; then A191:
(rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) =
(((rng h1) \/ (rng f)) /\ (rng (g2 | m))) \/ {}
by A148, XBOOLE_1:23
.=
{} \/ ((rng f) /\ (rng (g2 | m)))
by A170, XBOOLE_1:23
.=
(rng f) /\ (rng (g2 | m))
;
A192:
rng f c= rng g1
then A194:
(rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) c= (rng g1) /\ (rng g2)
by A36, A191, XBOOLE_1:27;
A195:
0 + 1
< width G1
by A5, A68, XREAL_1:8;
then A196:
(
len (DelCol G1,1) = len G1 &
len (DelCol G1,(width G1)) = len G1 &
Seg (len ((h1 ^ f) ^ h2)) = dom ((h1 ^ f) ^ h2) )
by A14, A15, FINSEQ_1:def 3, GOBOARD1:def 10;
then A197:
( 1
in dom ((h1 ^ f) ^ h2) &
len ((h1 ^ f) ^ h2) in dom ((h1 ^ f) ^ h2) )
by A135, A136, FINSEQ_1:3;
A198:
dom (DelCol G1,1) =
Seg (len G1)
by A196, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
thus
(rng g1) /\ (rng g2) <> {}
:: thesis: verumproof
per cases
( (rng f) /\ (rng (Col G1,1)) = {} or (rng f) /\ (rng (Col G1,1)) <> {} )
;
suppose
(rng f) /\ (rng (Col G1,1)) = {}
;
:: thesis: (rng g1) /\ (rng g2) <> {} then
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col G1,1)) = {}
by A14, A149;
then A199:
rng ((h1 ^ f) ^ h2) misses rng (Col G1,1)
by XBOOLE_0:def 7;
defpred S7[
Nat]
means ( $1
in dom (g2 | m) &
(g2 | m) /. $1
in rng (Col G1,1) );
A200:
for
m being
Nat st
S7[
m] holds
m <= len (g2 | m)
by FINSEQ_3:27;
A201:
ex
m being
Nat st
S7[
m]
consider m being
Nat such that A202:
(
S7[
m] & ( for
k being
Nat st
S7[
k] holds
k <= m ) )
from NAT_1:sch 6(A200, A201);
A203:
for
k being
Element of
NAT st
S7[
k] holds
k <= m
by A202;
reconsider m =
m as
Element of
NAT by ORDINAL1:def 13;
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:18;
deffunc H3(
Nat)
-> Element of the
carrier of
(TOP-REAL 2) =
(g2 | m) /. (m + $1);
consider t being
FinSequence of
(TOP-REAL 2) such that A206:
(
len t = ll & ( for
n being
Nat st
n in dom t holds
t /. n = H3(
n) ) )
from FINSEQ_4:sch 2();
A207:
Seg (len t) = dom t
by FINSEQ_1:def 3;
A208:
dom t = Seg ll
by A206, FINSEQ_1:def 3;
A209:
for
n being
Element of
NAT st
n in dom t holds
m + n in dom (g2 | m)
A210:
rng t c= rng (g2 | m)
reconsider t =
t as
FinSequence of
(TOP-REAL 2) ;
set D =
DelCol G1,1;
A212:
width (DelCol G1,1) = k
by A5, A14, A67, GOBOARD1:26, NAT_1:3;
0 <> width (DelCol G1,1)
by GOBOARD1:def 5;
then
0 < width (DelCol G1,1)
by NAT_1:3;
then A213:
0 + 1
<= width (DelCol G1,1)
by NAT_1:13;
m + 1
<= len (g2 | m)
by A204, NAT_1:13;
then A214:
1
<= len t
by A206, XREAL_1:21;
then
1
in Seg ll
by A206, FINSEQ_1:3;
then A215:
t /. 1
= (g2 | m) /. (m + 1)
by A206, A207;
(
Col (DelCol G1,1),1
= Col G1,
(1 + 1) & 1
+ 1
in Seg (width G1) )
by A5, A14, A68, A212, A213, GOBOARD1:30;
then A216:
t /. 1
in rng (Col (DelCol G1,1),1)
by A9, A10, A12, A14, A202, A203, A215, GOBOARD1:48;
len t in Seg ll
by A206, A214, FINSEQ_1:3;
then t /. (len t) =
(g2 | m) /. (m + ll)
by A206, A207
.=
(g2 | m) /. (len (g2 | m))
;
then A217:
t /. (len t) in rng (Col (DelCol G1,1),(width (DelCol G1,1)))
by A5, A12, A14, A68, A212, A213, GOBOARD1:30;
A218:
Indices (DelCol G1,1) = [:(dom (DelCol G1,1)),(Seg (width (DelCol G1,1))):]
by MATRIX_1:def 5;
A219:
now let n be
Element of
NAT ;
:: thesis: ( 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 A220:
n in dom t
;
:: thesis: 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 A209;
then consider i1,
i2 being
Element of
NAT such that A221:
(
[i1,i2] in Indices G1 &
(g2 | m) /. (m + n) = G1 * i1,
i2 )
by A10, GOBOARD1:def 11;
take i1 =
i1;
:: thesis: ex l being Element of NAT st
( [i1,l] in Indices (DelCol G1,1) & t /. n = (DelCol G1,1) * i1,l )reconsider Ci2 =
Col G1,
i2 as
FinSequence of
(TOP-REAL 2) ;
A222:
(
i1 in dom G1 &
i2 in Seg (width G1) &
t /. n = (g2 | m) /. (m + n) &
m + n in dom (g2 | m) )
by A87, A206, A209, A220, A221, ZFMISC_1:106;
len Ci2 = len G1
by MATRIX_1:def 9;
then A223:
dom Ci2 =
Seg (len G1)
by FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
then
Ci2 /. i1 = Ci2 . i1
by A222, PARTFUN1:def 8;
then
(
Ci2 /. i1 = G1 * i1,
i2 &
dom (Col G1,i2) = dom (Col G1,i2) &
len (Col G1,i2) = len G1 )
by A222, MATRIX_1:def 9;
then A224:
(g2 | m) /. (m + n) in rng (Col G1,i2)
by A221, A222, A223, PARTFUN2:4;
then A226:
( 1
<> i2 & 1
<= i2 &
i2 <= width G1 )
by A222, FINSEQ_1:3;
then A227:
1
< i2
by XXREAL_0:1;
reconsider l =
i2 - 1 as
Element of
NAT by A226, INT_1:18;
take l =
l;
:: thesis: ( [i1,l] in Indices (DelCol G1,1) & t /. n = (DelCol G1,1) * i1,l )
1
+ 1
<= i2
by A227, NAT_1:13;
then A228:
( 1
<= l &
l <= width (DelCol G1,1) &
l + 1
= i2 )
by A5, A212, A226, XREAL_1:21, XREAL_1:22;
then
l in Seg (width (DelCol G1,1))
by FINSEQ_1:3;
hence
[i1,l] in Indices (DelCol G1,1)
by A198, A218, A222, ZFMISC_1:106;
:: thesis: t /. n = (DelCol G1,1) * i1,lthus
t /. n = (DelCol G1,1) * i1,
l
by A5, A14, A68, A212, A221, A222, A228, GOBOARD1:32;
:: thesis: verum end; now let n be
Element of
NAT ;
:: thesis: ( 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 A229:
(
n in dom t &
n + 1
in dom t )
;
:: thesis: 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))then A230:
(
t /. n = (g2 | m) /. (m + n) &
t /. (n + 1) = (g2 | m) /. (m + (n + 1)) )
by A206;
let i1,
i2,
j1,
j2 be
Element of
NAT ;
:: thesis: ( [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 A231:
(
[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 )
;
:: thesis: 1 = (abs (i1 - j1)) + (abs (i2 - j2))then A232:
(
i1 in dom (DelCol G1,1) &
i2 in Seg k &
j1 in dom (DelCol G1,1) &
j2 in Seg k &
m + (n + 1) = (m + n) + 1 )
by A212, A218, ZFMISC_1:106;
then
( 1
<= i2 &
i2 <= k & 1
<= j2 &
j2 <= k )
by FINSEQ_1:3;
then A233:
(
(g2 | m) /. (m + n) = G1 * i1,
(i2 + 1) &
(g2 | m) /. ((m + n) + 1) = G1 * j1,
(j2 + 1) &
i2 + 1
in Seg (width G1) &
j2 + 1
in Seg (width G1) )
by A5, A14, A68, A198, A230, A231, A232, GOBOARD1:32;
then A234:
(
[i1,(i2 + 1)] in Indices G1 &
[j1,(j2 + 1)] in Indices G1 )
by A87, A198, A232, ZFMISC_1:106;
(
m + n in dom (g2 | m) &
(m + n) + 1
in dom (g2 | m) )
by A209, A229, A232;
hence 1 =
(abs (i1 - j1)) + (abs ((i2 + 1) - (j2 + 1)))
by A10, A233, A234, GOBOARD1:def 11
.=
(abs (i1 - j1)) + (abs (i2 - j2))
;
:: thesis: verum end; then A235:
t is_sequence_on DelCol G1,1
by A219, GOBOARD1:def 11;
(
(h1 ^ f) ^ h2 is_sequence_on DelCol G1,1 &
((h1 ^ f) ^ h2) /. 1
in rng (Line (DelCol G1,1),1) &
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line (DelCol G1,1),(len (DelCol G1,1))) )
by A14, A16, A17, A121, A122, A137, A195, A196, A197, A199, GOBOARD1:37, GOBOARD1:41;
then A236:
(rng ((h1 ^ f) ^ h2)) /\ (rng t) <> {}
by A4, A68, A135, A136, A212, A214, A216, A217, A235;
consider x being
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng t);
(rng ((h1 ^ f) ^ h2)) /\ (rng t) c= (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m))
by A210, XBOOLE_1:26;
then
x in (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m))
by A236, TARSKI:def 3;
hence
(rng g1) /\ (rng g2) <> {}
by A194;
:: thesis: verum end; suppose A237:
(rng f) /\ (rng (Col G1,1)) <> {}
;
:: thesis: (rng g1) /\ (rng g2) <> {} set D =
DelCol G1,
(width G1);
A238:
0 + 1
< k + 1
by A68, XREAL_1:8;
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))) = {}
;
:: thesis: (rng g1) /\ (rng g2) <> {} then
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col G1,(width G1))) = {}
by A15, A149;
then A239:
rng ((h1 ^ f) ^ h2) misses rng (Col G1,(width G1))
by XBOOLE_0:def 7;
consider t being
FinSequence of
(TOP-REAL 2) such that A240:
(
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) &
rng t c= rng (g2 | m) )
by A5, A9, A10, A11, A12, A238, GOBOARD1:51;
A241:
width (DelCol G1,(width G1)) = k
by A5, A15, A67, GOBOARD1:26, 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)))) &
(h1 ^ f) ^ h2 is_sequence_on DelCol G1,
(width G1) )
by A15, A16, A17, A121, A122, A137, A195, A196, A197, A239, GOBOARD1:37, GOBOARD1:41;
then A242:
(rng ((h1 ^ f) ^ h2)) /\ (rng t) <> {}
by A4, A68, A135, A136, A240, A241;
consider x being
Element of
(rng ((h1 ^ f) ^ h2)) /\ (rng t);
(rng ((h1 ^ f) ^ h2)) /\ (rng t) c= (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m))
by A240, XBOOLE_1:26;
then
x in (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m))
by A242, TARSKI:def 3;
hence
(rng g1) /\ (rng g2) <> {}
by A194;
:: thesis: verum end; suppose A243:
(rng f) /\ (rng (Col G1,(width G1))) <> {}
;
:: thesis: (rng g1) /\ (rng g2) <> {} A244:
f is_sequence_on G1
by A95, A106, GOBOARD1:def 11;
then consider t being
FinSequence of
(TOP-REAL 2) such that A245:
(
rng t c= rng f &
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 A237, A243, GOBOARD1:52;
consider tt being
FinSequence of
(TOP-REAL 2) such that A246:
(
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) &
rng tt c= rng t )
by A5, A238, A245, GOBOARD1:51;
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) );
consider pf being
Nat such that A251:
(
S7[
pf] & ( for
n being
Nat st
S7[
n] holds
pf <= n ) )
from NAT_1:sch 5(A247);
consider pl being
Nat such that A252:
(
S8[
pl] & ( for
n being
Nat st
S8[
n] holds
pl <= n ) )
from NAT_1:sch 5(A249);
reconsider pf =
pf,
pl =
pl as
Element of
NAT by ORDINAL1:def 13;
A253:
pl <> pf
by A26, A28, A69, A251, A252, GOBOARD1:19;
A254:
( 1
<= pf &
pf <= len (g2 | m) & 1
<= pl &
pl <= len (g2 | m) )
by A251, A252, FINSEQ_3:27;
then A255:
( 1
<= (len (g2 | m)) - 1 & 1
<= len (g2 | m) )
by A8, GOBOARD1:38, XREAL_1:21;
reconsider lg =
(len (g2 | m)) - 1 as
Element of
NAT by A9, INT_1:18;
lg <= len (g2 | m)
by XREAL_1:45;
then A256:
(
lg in dom (g2 | m) &
len (g2 | m) in dom (g2 | m) &
lg + 1
= len (g2 | m) )
by A255, FINSEQ_3:27;
reconsider C =
Col G1,
(width G1),
Li =
Line G1,
mi,
La =
Line G1,
ma as
FinSequence of
(TOP-REAL 2) ;
A257:
dom (g2 | m) c= dom g2
by A6, A19, A34, A35, FINSEQ_1:7;
len C = len G1
by MATRIX_1:def 9;
then A258:
dom C =
Seg (len G1)
by FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
consider K1 being
Element of
NAT such that A259:
(
K1 in dom Li &
(g2 | m) /. pf = Li /. K1 )
by A251, PARTFUN2:4;
A260:
Seg (len Li) = dom Li
by FINSEQ_1:def 3;
reconsider CK1 =
Col G1,
K1 as
FinSequence of
(TOP-REAL 2) ;
A261:
len Li = width G1
by MATRIX_1:def 8;
A262:
Li /. K1 = Li . K1
by A259, PARTFUN1:def 8;
then A263:
(
K1 in Seg (width G1) &
(g2 | m) /. pf = G1 * mi,
K1 )
by A259, A260, A261, MATRIX_1:def 8;
now assume A264:
pf = len (g2 | m)
;
:: thesis: contradictionconsider i2 being
Element of
NAT such that A265:
(
i2 in dom C &
C /. i2 = (g2 | m) /. (len (g2 | m)) )
by A12, PARTFUN2:4;
C /. i2 = C . i2
by A265, PARTFUN1:def 8;
then A266:
(
i2 in dom G1 &
(g2 | m) /. (len (g2 | m)) = G1 * i2,
(width G1) )
by A258, A265, MATRIX_1:def 9;
A267:
[i2,(width G1)] in Indices G1
by A15, A87, A258, A265, ZFMISC_1:106;
[mi,K1] in Indices G1
by A26, A87, A259, A260, A261, ZFMISC_1:106;
then A268:
(
i2 = mi &
width G1 = K1 )
by A263, A264, A266, A267, GOBOARD1:21;
consider n1,
n2 being
Element of
NAT such that A269:
(
[n1,n2] in Indices G1 &
(g2 | m) /. lg = G1 * n1,
n2 )
by A10, A256, GOBOARD1:def 11;
A270:
(abs (n1 - mi)) + (abs (n2 - (width G1))) = 1
by A10, A256, A266, A267, A268, A269, GOBOARD1:def 11;
A271:
(
n1 in dom G1 &
n2 in Seg (width G1) )
by A87, A269, ZFMISC_1:106;
now per cases
( ( abs (n1 - mi) = 1 & n2 = width G1 ) or ( abs (n2 - (width G1)) = 1 & n1 = mi ) )
by A270, GOBOARD1:2;
suppose A272:
(
abs (n1 - mi) = 1 &
n2 = width G1 )
;
:: thesis: contradictionA273:
dom C =
Seg (len C)
by FINSEQ_1:def 3
.=
Seg (len G1)
by MATRIX_1:def 9
.=
dom G1
by FINSEQ_1:def 3
;
then
C /. n1 = C . n1
by A271, PARTFUN1:def 8;
then
(g2 | m) /. lg = C /. n1
by A269, A271, A272, MATRIX_1:def 9;
then
(
(g2 | m) /. lg in rng C &
0 < 1 &
(g2 | m) /. lg = g2 /. lg )
by A8, A19, A35, A256, A271, A273, FINSEQ_4:86, PARTFUN2:4;
hence
contradiction
by A8, A35, A256, A257, XREAL_1:46;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end; then A276:
pf < len (g2 | m)
by A254, XXREAL_0:1;
consider K2 being
Element of
NAT such that A277:
(
K2 in dom Lma &
(g2 | m) /. pl = Lma /. K2 )
by A252, PARTFUN2:4;
A278:
Seg (len Lma) = dom Lma
by FINSEQ_1:def 3;
reconsider CK2 =
Col G1,
K2 as
FinSequence of
(TOP-REAL 2) ;
A279:
len Lma = width G1
by MATRIX_1:def 8;
A280:
Lma /. K2 = Lma . K2
by A277, PARTFUN1:def 8;
then A281:
(
K2 in Seg (width G1) &
(g2 | m) /. pl = G1 * ma,
K2 )
by A277, A278, A279, MATRIX_1:def 8;
now assume A282:
pl = len (g2 | m)
;
:: thesis: contradictionconsider i2 being
Element of
NAT such that A283:
(
i2 in dom C &
C /. i2 = (g2 | m) /. (len (g2 | m)) )
by A12, PARTFUN2:4;
A284:
dom C =
Seg (len C)
by FINSEQ_1:def 3
.=
Seg (len G1)
by MATRIX_1:def 9
.=
dom G1
by FINSEQ_1:def 3
;
C /. i2 = C . i2
by A283, PARTFUN1:def 8;
then A285:
(
i2 in dom G1 &
(g2 | m) /. (len (g2 | m)) = G1 * i2,
(width G1) )
by A283, A284, MATRIX_1:def 9;
A286:
[i2,(width G1)] in Indices G1
by A15, A87, A283, A284, ZFMISC_1:106;
[ma,K2] in Indices G1
by A28, A87, A277, A278, A279, ZFMISC_1:106;
then A287:
(
i2 = ma &
width G1 = K2 )
by A281, A282, A285, A286, GOBOARD1:21;
consider n1,
n2 being
Element of
NAT such that A288:
(
[n1,n2] in Indices G1 &
(g2 | m) /. lg = G1 * n1,
n2 )
by A10, A256, GOBOARD1:def 11;
A289:
(abs (n1 - ma)) + (abs (n2 - (width G1))) = 1
by A10, A256, A285, A286, A287, A288, GOBOARD1:def 11;
A290:
(
n1 in dom G1 &
n2 in Seg (width G1) )
by A87, A288, ZFMISC_1:106;
now per cases
( ( abs (n1 - ma) = 1 & n2 = width G1 ) or ( abs (n2 - (width G1)) = 1 & n1 = ma ) )
by A289, GOBOARD1:2;
suppose A291:
(
abs (n1 - ma) = 1 &
n2 = width G1 )
;
:: thesis: contradictionA292:
dom C =
Seg (len C)
by FINSEQ_1:def 3
.=
Seg (len G1)
by MATRIX_1:def 9
.=
dom G1
by FINSEQ_1:def 3
;
then
C /. n1 = C . n1
by A290, PARTFUN1:def 8;
then
(g2 | m) /. lg = C /. n1
by A288, A290, A291, MATRIX_1:def 9;
then
(
(g2 | m) /. lg in rng C &
0 < 1 &
(g2 | m) /. lg = g2 /. lg )
by A8, A19, A35, A256, A290, A292, FINSEQ_4:86, PARTFUN2:4;
hence
contradiction
by A8, A35, A256, A257, XREAL_1:46;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end; then A295:
pl < len (g2 | m)
by A254, XXREAL_0:1;
deffunc H3(
Nat)
-> Element of the
carrier of
(TOP-REAL 2) =
G1 * $1,
K1;
consider h1 being
FinSequence of
(TOP-REAL 2) such that A296:
(
len h1 = l1 & ( for
n being
Nat st
n in dom h1 holds
h1 /. n = H3(
n) ) )
from FINSEQ_4:sch 2();
A297:
Seg (len h1) = dom h1
by FINSEQ_1:def 3;
deffunc H4(
Nat)
-> Element of the
carrier of
(TOP-REAL 2) =
G1 * (ma + $1),
K2;
consider h2 being
FinSequence of
(TOP-REAL 2) such that A298:
(
len h2 = l2 & ( for
n being
Nat st
n in dom h2 holds
h2 /. n = H4(
n) ) )
from FINSEQ_4:sch 2();
A299:
Seg (len h2) = dom h2
by FINSEQ_1:def 3;
A303:
now let n be
Element of
NAT ;
:: thesis: ( n in dom h1 implies ex i, K1 being Element of NAT st
( [i,K1] in Indices G1 & h1 /. n = G1 * i,K1 ) )assume
n in dom h1
;
:: thesis: ex i, K1 being Element of NAT st
( [i,K1] in Indices G1 & h1 /. n = G1 * i,K1 )then A304:
(
h1 /. n = G1 * n,
K1 &
n in dom G1 )
by A296, A300;
take i =
n;
:: thesis: ex K1 being Element of NAT st
( [i,K1] in Indices G1 & h1 /. n = G1 * i,K1 )take K1 =
K1;
:: thesis: ( [i,K1] in Indices G1 & h1 /. n = G1 * i,K1 )thus
(
[i,K1] in Indices G1 &
h1 /. n = G1 * i,
K1 )
by A87, A259, A260, A261, A304, ZFMISC_1:106;
:: thesis: verum end; A305:
now let n be
Element of
NAT ;
:: thesis: ( 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
n in dom h2
;
:: thesis: ex m being Element of NAT ex K2 being Element of NAT st
( [m,K2] in Indices G1 & h2 /. n = G1 * m,K2 )then A306:
(
h2 /. n = G1 * (ma + n),
K2 &
ma + n in dom G1 )
by A298, A302;
take m =
ma + n;
:: thesis: ex K2 being Element of NAT st
( [m,K2] in Indices G1 & h2 /. n = G1 * m,K2 )take K2 =
K2;
:: thesis: ( [m,K2] in Indices G1 & h2 /. n = G1 * m,K2 )thus
(
[m,K2] in Indices G1 &
h2 /. n = G1 * m,
K2 )
by A87, A277, A278, A279, A306, ZFMISC_1:106;
:: thesis: verum end; A307:
now let n be
Element of
NAT ;
:: thesis: ( 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
(
n in dom h1 &
n + 1
in dom h1 )
;
:: thesis: 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)) = 1then A308:
(
n in dom G1 &
n + 1
in dom G1 &
h1 /. n = G1 * n,
K1 &
h1 /. (n + 1) = G1 * (n + 1),
K1 )
by A296, A300;
then A309:
(
[n,K1] in Indices G1 &
[(n + 1),K1] in Indices G1 )
by A87, A259, A260, A261, ZFMISC_1:106;
let i1,
i2,
j1,
j2 be
Element of
NAT ;
:: thesis: ( [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
(
[i1,i2] in Indices G1 &
[j1,j2] in Indices G1 &
h1 /. n = G1 * i1,
i2 &
h1 /. (n + 1) = G1 * j1,
j2 )
;
:: thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1then
(
i1 = n &
i2 = K1 &
j1 = n + 1 &
j2 = K1 &
0 <= 1 )
by A308, A309, GOBOARD1:21;
hence (abs (i1 - j1)) + (abs (i2 - j2)) =
(abs ((n - n) + (- 1))) + 0
by ABSVALUE:7
.=
abs 1
by COMPLEX1:138
.=
1
by ABSVALUE:def 1
;
:: thesis: verum end; A310:
now let n be
Element of
NAT ;
:: thesis: ( 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
(
n in dom h2 &
n + 1
in dom h2 )
;
:: thesis: 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)) = 1then A311:
(
ma + n in dom G1 &
ma + (n + 1) in dom G1 &
h2 /. n = G1 * (ma + n),
K2 &
h2 /. (n + 1) = G1 * (ma + (n + 1)),
K2 &
ma + (n + 1) = (ma + n) + 1 )
by A298, A302;
then A312:
(
[(ma + n),K2] in Indices G1 &
[((ma + n) + 1),K2] in Indices G1 )
by A87, A277, A278, A279, ZFMISC_1:106;
let i1,
i2,
j1,
j2 be
Element of
NAT ;
:: thesis: ( [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
(
[i1,i2] in Indices G1 &
[j1,j2] in Indices G1 &
h2 /. n = G1 * i1,
i2 &
h2 /. (n + 1) = G1 * j1,
j2 )
;
:: thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1then
(
i1 = ma + n &
i2 = K2 &
j1 = (ma + n) + 1 &
j2 = K2 &
0 <= 1 )
by A311, A312, GOBOARD1:21;
hence (abs (i1 - j1)) + (abs (i2 - j2)) =
(abs (((ma + n) - (ma + n)) + (- 1))) + 0
by ABSVALUE:7
.=
abs 1
by COMPLEX1:138
.=
1
by ABSVALUE:def 1
;
:: thesis: verum end; 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 );
A313:
S9[
0 ]
by FINSEQ_3:27;
A314:
for
k being
Element of
NAT st
S9[
k] holds
S9[
k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S9[k] implies S9[k + 1] )
assume A315:
S9[
k]
;
:: thesis: S9[k + 1]
assume A316:
k + 1
in dom f
;
:: thesis: 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 ;
:: thesis: ( m in dom G1 & f /. (k + 1) in rng (Line G1,m) implies mi <= m )
assume A317:
(
m in dom G1 &
f /. (k + 1) in rng (Line G1,m) )
;
:: thesis: mi <= m
now per cases
( k = 0 or k <> 0 )
;
suppose
k <> 0
;
:: thesis: mi <= mthen
(
0 < k &
k <= k + 1 &
k + 1
<= len f )
by A316, FINSEQ_3:27, NAT_1:3, NAT_1:11;
then A320:
(
0 + 1
<= k &
k <= len f )
by NAT_1:13;
then A321:
k in dom f
by FINSEQ_3:27;
then consider i1,
i2 being
Element of
NAT such that A322:
(
[i1,i2] in Indices G1 &
f /. k = G1 * i1,
i2 )
by A95;
reconsider Li1 =
Line G1,
i1 as
FinSequence of
(TOP-REAL 2) ;
A323:
Seg (len Li1) = dom Li1
by FINSEQ_1:def 3;
A324:
(
i1 in dom G1 &
i2 in Seg (width G1) )
by A87, A322, ZFMISC_1:106;
A325:
len Li1 = width G1
by MATRIX_1:def 8;
then A326:
Li1 /. i2 = Li1 . i2
by A323, A324, PARTFUN1:def 8;
then
f /. k = Li1 /. i2
by A322, A324, MATRIX_1:def 8;
then A327:
f /. k in rng Li1
by A323, A324, A325, PARTFUN2:4;
then A328:
mi <= i1
by A315, A320, A324, FINSEQ_3:27;
consider j1,
j2 being
Element of
NAT such that A329:
(
[j1,j2] in Indices G1 &
f /. (k + 1) = G1 * j1,
j2 )
by A95, A316;
reconsider Lj1 =
Line G1,
j1 as
FinSequence of
(TOP-REAL 2) ;
A330:
Seg (len Lj1) = dom Lj1
by FINSEQ_1:def 3;
A331:
(
j1 in dom G1 &
j2 in Seg (width G1) )
by A87, A329, ZFMISC_1:106;
A332:
len Lj1 = width G1
by MATRIX_1:def 8;
then
Lj1 /. j2 = Lj1 . j2
by A330, A331, PARTFUN1:def 8;
then
f /. (k + 1) = Lj1 /. j2
by A329, A331, MATRIX_1:def 8;
then A333:
f /. (k + 1) in rng Lj1
by A330, A331, A332, PARTFUN2:4;
now per cases
( mi = i1 or mi < i1 )
by A328, XXREAL_0:1;
suppose A334:
mi = i1
;
:: thesis: mi <= mA335:
(
f /. k = (g1 | mi1) /. (w + k) &
(g1 | mi1) /. (w + k) = g1 /. (w + k) &
w + k in dom g1 )
by A74, A78, A79, A321;
g1 /. (w + k) =
(g1 | mi1) /. (w + k)
by A74, A79, A321
.=
f /. k
by A78, A79, A321
.=
Li1 /. i2
by A322, A324, A326, MATRIX_1:def 8
;
then A336:
g1 /. (w + k) in rng (Line G1,mi)
by A323, A324, A325, A334, PARTFUN2:4;
w + 1
<= w + k
by A320, XREAL_1:9;
then
(
w + k <= ma1 &
ma1 <= w + k )
by A32, A335, A336;
then
w + k = ma1
by XXREAL_0:1;
then A337:
ma1 + 1
= w + (k + 1)
;
A338:
(
f /. (k + 1) = (g1 | mi1) /. (w + (k + 1)) &
(g1 | mi1) /. (w + (k + 1)) = g1 /. (w + (k + 1)) &
w + (k + 1) in dom g1 &
(ma - 1) + (k + 1) = ((ma - 1) + k) + 1 )
by A74, A78, A79, A316;
(
mi + 1
<= ma &
mi <= mi + 1 )
by A71, NAT_1:13;
then
( 1
<= mi + 1 &
mi + 1
<= len G1 )
by A29, XXREAL_0:2;
then A339:
mi + 1
in dom G1
by FINSEQ_3:27;
then
f /. (k + 1) in rng (Line G1,(mi + 1))
by A5, A26, A32, A33, A337, A338, GOBOARD1:44;
then
(
m = mi + 1 &
mi <= mi + 1 )
by A317, A339, GOBOARD1:19, NAT_1:11;
hence
mi <= m
;
:: thesis: verum end; hence
mi <= m
;
:: thesis: verum end;
hence
mi <= m
;
:: thesis: verum
end; A342:
for
n being
Element of
NAT holds
S9[
n]
from NAT_1:sch 1(A313, A314);
A343:
(rng h1) /\ (rng tt) = {}
proof
assume A344:
not
(rng h1) /\ (rng tt) = {}
;
:: thesis: contradiction
consider x being
Element of
(rng h1) /\ (rng tt);
A345:
(
x in rng h1 &
x in rng tt )
by A344, XBOOLE_0:def 4;
then
x in rng t
by A246;
then consider i1 being
Element of
NAT such that A346:
(
i1 in dom f &
f /. i1 = x )
by A245, PARTFUN2:4;
consider n1,
n2 being
Element of
NAT such that A347:
(
[n1,n2] in Indices G1 &
f /. i1 = G1 * n1,
n2 )
by A95, A346;
reconsider Ln1 =
Line G1,
n1 as
FinSequence of
(TOP-REAL 2) ;
A348:
Seg (len Ln1) = dom Ln1
by FINSEQ_1:def 3;
A349:
(
n1 in dom G1 &
n2 in Seg (width G1) )
by A87, A347, ZFMISC_1:106;
A350:
len Ln1 = width G1
by MATRIX_1:def 8;
then
Ln1 /. n2 = Ln1 . n2
by A348, A349, PARTFUN1:def 8;
then
f /. i1 = Ln1 /. n2
by A347, A349, MATRIX_1:def 8;
then
f /. i1 in rng Ln1
by A348, A349, A350, PARTFUN2:4;
then A351:
mi <= n1
by A342, A346, A349;
consider i2 being
Element of
NAT such that A352:
(
i2 in dom h1 &
h1 /. i2 = x )
by A345, PARTFUN2:4;
A353:
Seg (len h1) = dom h1
by FINSEQ_1:def 3;
A354:
(
x = G1 * i2,
K1 &
i2 in dom G1 )
by A296, A300, A352;
then
[i2,K1] in Indices G1
by A87, A259, A260, A261, ZFMISC_1:106;
then A355:
(
i2 = n1 &
n2 = K1 )
by A346, A347, A354, GOBOARD1:21;
(
l1 < mi &
i2 <= l1 )
by A296, A352, A353, FINSEQ_1:3, XREAL_1:46;
hence
contradiction
by A351, A355, XXREAL_0:2;
:: thesis: 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 );
A356:
S10[
0 ]
by FINSEQ_3:27;
A357:
for
k being
Element of
NAT st
S10[
k] holds
S10[
k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S10[k] implies S10[k + 1] )
assume A358:
S10[
k]
;
:: thesis: S10[k + 1]
assume A359:
k + 1
in dom f
;
:: thesis: 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 ;
:: thesis: ( m in dom G1 & f /. (k + 1) in rng (Line G1,m) implies m <= ma )
assume A360:
(
m in dom G1 &
f /. (k + 1) in rng (Line G1,m) )
;
:: thesis: m <= ma
now per cases
( k = 0 or k <> 0 )
;
suppose
k <> 0
;
:: thesis: m <= mathen A362:
(
0 < k &
k <= k + 1 &
k + 1
<= len f )
by A85, A359, FINSEQ_1:3, NAT_1:3, NAT_1:11;
then A363:
(
0 + 1
<= k &
k <= len f )
by NAT_1:13;
then A364:
k in dom f
by FINSEQ_3:27;
then consider i1,
i2 being
Element of
NAT such that A365:
(
[i1,i2] in Indices G1 &
f /. k = G1 * i1,
i2 )
by A95;
reconsider Li1 =
Line G1,
i1 as
FinSequence of
(TOP-REAL 2) ;
A366:
Seg (len Li1) = dom Li1
by FINSEQ_1:def 3;
A367:
(
i1 in dom G1 &
i2 in Seg (width G1) )
by A87, A365, ZFMISC_1:106;
A368:
len Li1 = width G1
by MATRIX_1:def 8;
then
Li1 /. i2 = Li1 . i2
by A366, A367, PARTFUN1:def 8;
then
f /. k = Li1 /. i2
by A365, A367, MATRIX_1:def 8;
then A369:
f /. k in rng Li1
by A366, A367, A368, PARTFUN2:4;
then A370:
i1 <= ma
by A358, A363, A367, FINSEQ_3:27;
consider j1,
j2 being
Element of
NAT such that A371:
(
[j1,j2] in Indices G1 &
f /. (k + 1) = G1 * j1,
j2 )
by A95, A359;
reconsider Lj1 =
Line G1,
j1 as
FinSequence of
(TOP-REAL 2) ;
A372:
Seg (len Lj1) = dom Lj1
by FINSEQ_1:def 3;
A373:
(
j1 in dom G1 &
j2 in Seg (width G1) )
by A87, A371, ZFMISC_1:106;
A374:
len Lj1 = width G1
by MATRIX_1:def 8;
then
Lj1 /. j2 = Lj1 . j2
by A372, A373, PARTFUN1:def 8;
then
f /. (k + 1) = Lj1 /. j2
by A371, A373, MATRIX_1:def 8;
then A375:
f /. (k + 1) in rng Lj1
by A372, A373, A374, PARTFUN2:4;
then A376:
j1 = m
by A360, A373, GOBOARD1:19;
now per cases
( ma = i1 or i1 < ma )
by A370, XXREAL_0:1;
case A377:
ma = i1
;
:: thesis: contradictionA378:
(
f /. k = (g1 | mi1) /. (w + k) &
w is
Element of
NAT &
(g1 | mi1) /. (w + k) = g1 /. (w + k) &
w + k in dom g1 &
f /. (k + 1) = (g1 | mi1) /. (w + (k + 1)) &
(g1 | mi1) /. (w + (k + 1)) = g1 /. (w + (k + 1)) &
w + (k + 1) in dom g1 &
(ma - 1) + (k + 1) = ((ma - 1) + k) + 1 )
by A74, A78, A79, A359, A364;
A379:
w + 1
<= w + k
by A363, XREAL_1:9;
ma1 <> w + k
by A26, A28, A32, A69, A369, A377, A378, GOBOARD1:19;
then
ma1 < w + k
by A379, XXREAL_0:1;
then A380:
mi1 <= w + k
by A73, A369, A377, A378;
w + k <= mi1
by A78, A102, A363, XREAL_1:9;
then
w + k = mi1
by A380, XXREAL_0:1;
hence
contradiction
by A78, A362, NAT_1:13;
:: thesis: verum end; hence
m <= ma
;
:: thesis: verum end;
hence
m <= ma
;
:: thesis: verum
end; A383:
for
n being
Element of
NAT holds
S10[
n]
from NAT_1:sch 1(A356, A357);
A384:
(rng h2) /\ (rng tt) = {}
proof
assume A385:
not
(rng h2) /\ (rng tt) = {}
;
:: thesis: contradiction
consider x being
Element of
(rng h2) /\ (rng tt);
A386:
(
x in rng h2 &
x in rng tt )
by A385, XBOOLE_0:def 4;
then
x in rng t
by A246;
then consider i1 being
Element of
NAT such that A387:
(
i1 in dom f &
f /. i1 = x )
by A245, PARTFUN2:4;
consider n1,
n2 being
Element of
NAT such that A388:
(
[n1,n2] in Indices G1 &
f /. i1 = G1 * n1,
n2 )
by A95, A387;
reconsider Ln1 =
Line G1,
n1 as
FinSequence of
(TOP-REAL 2) ;
A389:
Seg (len Ln1) = dom Ln1
by FINSEQ_1:def 3;
A390:
(
n1 in dom G1 &
n2 in Seg (width G1) )
by A87, A388, ZFMISC_1:106;
A391:
len Ln1 = width G1
by MATRIX_1:def 8;
then
Ln1 /. n2 = Ln1 . n2
by A389, A390, PARTFUN1:def 8;
then
f /. i1 = Ln1 /. n2
by A388, A390, MATRIX_1:def 8;
then
f /. i1 in rng Ln1
by A389, A390, A391, PARTFUN2:4;
then A392:
n1 <= ma
by A383, A387, A390;
consider i2 being
Element of
NAT such that A393:
(
i2 in dom h2 &
h2 /. i2 = x )
by A386, PARTFUN2:4;
A394:
(
x = G1 * (ma + i2),
K2 &
ma + i2 in dom G1 )
by A298, A302, A393;
then
[(ma + i2),K2] in Indices G1
by A87, A277, A278, A279, ZFMISC_1:106;
then A395:
(
ma + i2 = n1 &
n2 = K2 )
by A387, A388, A394, GOBOARD1:21;
0 + 1
<= i2
by A393, FINSEQ_3:27;
then
0 < i2
by NAT_1:13;
hence
contradiction
by A392, A395, XREAL_1:31;
:: thesis: verum
end; now per cases
( pf < pl or pl < pf )
by A253, XXREAL_0:1;
suppose A396:
pf < pl
;
:: thesis: (rng g1) /\ (rng g2) <> {} set F1 =
(g2 | m) | pl;
(
pf <= pl &
pl <= pl + 1 )
by A396, NAT_1:11;
then reconsider LL =
(pl + 1) - pf as
Element of
NAT by INT_1:18, XXREAL_0:2;
reconsider w1 =
pf - 1 as
Element of
NAT by A254, INT_1:18;
A397:
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) )
defpred S11[
Nat,
Element of
(TOP-REAL 2)]
means $2
= ((g2 | m) | pl) /. (w1 + $1);
A400:
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 A401:
(
len F = LL & ( for
n being
Nat st
n in Seg LL holds
S11[
n,
F /. n] ) )
from FINSEQ_4:sch 1(A400);
A402:
Seg (len F) = dom F
by FINSEQ_1:def 3;
set FF =
(h1 ^ F) ^ h2;
(
pf + 1
<= pl &
pl <= pl + 1 )
by A396, NAT_1:13;
then
(
pf + 1
<= pl + 1 &
dom F = dom F )
by XXREAL_0:2;
then A403:
( 1
<= LL &
len F = LL )
by A401, XREAL_1:21;
now let n be
Element of
NAT ;
:: thesis: ( n in dom F implies ex i, j being Element of NAT st
( [i,j] in Indices G1 & F /. n = G1 * i,j ) )assume
n in dom F
;
:: thesis: ex i, j being Element of NAT st
( [i,j] in Indices G1 & F /. n = G1 * i,j )then A404:
(
n in Seg LL &
dom F = Seg LL &
F /. n = ((g2 | m) | pl) /. (w1 + n) )
by A401, A402;
then A405:
(
w1 is
Element of
NAT &
w1 + n in dom (g2 | m) &
F /. n = (g2 | m) /. (w1 + n) )
by A397;
reconsider w =
w1 as
Element of
NAT ;
consider i,
j being
Element of
NAT such that A406:
(
[i,j] in Indices G1 &
(g2 | m) /. (w + n) = G1 * i,
j )
by A10, A405, GOBOARD1:def 11;
take i =
i;
:: thesis: ex j being Element of NAT st
( [i,j] in Indices G1 & F /. n = G1 * i,j )take j =
j;
:: thesis: ( [i,j] in Indices G1 & F /. n = G1 * i,j )thus
(
[i,j] in Indices G1 &
F /. n = G1 * i,
j )
by A397, A404, A406;
:: thesis: verum end; then A407:
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 A303, GOBOARD1:39;
A408:
w1 + LL = pl
;
A409:
now let n be
Element of
NAT ;
:: thesis: ( 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
(
n in dom F &
n + 1
in dom F )
;
:: thesis: 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)) = 1then
(
n in Seg LL &
n + 1
in Seg LL &
dom F = Seg LL &
F /. n = ((g2 | m) | pl) /. (w1 + n) &
F /. (n + 1) = ((g2 | m) | pl) /. (w1 + (n + 1)) &
w1 + (n + 1) = (w1 + n) + 1 )
by A401, A402;
then A410:
(
w1 is
Element of
NAT &
w1 + n in dom (g2 | m) &
F /. n = (g2 | m) /. (w1 + n) &
(w1 + n) + 1
in dom (g2 | m) &
F /. (n + 1) = (g2 | m) /. ((w1 + n) + 1) )
by A397;
let i1,
i2,
j1,
j2 be
Element of
NAT ;
:: thesis: ( [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
(
[i1,i2] in Indices G1 &
[j1,j2] in Indices G1 &
F /. n = G1 * i1,
i2 &
F /. (n + 1) = G1 * j1,
j2 )
;
:: thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1hence
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
by A10, A410, GOBOARD1:def 11;
:: thesis: verum end; A411:
now let i1,
i2,
j1,
j2 be
Element of
NAT ;
:: thesis: ( [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 A412:
(
[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 )
;
:: thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1then A413:
(
h1 /. (len h1) = G1 * l1,
K1 &
l1 in dom G1 )
by A296, A300;
then
[l1,K1] in Indices G1
by A87, A259, A260, A261, ZFMISC_1:106;
then A414:
(
i1 = l1 &
i2 = K1 &
0 <= 1 )
by A412, A413, GOBOARD1:21;
( 1
in Seg LL &
dom F = Seg LL &
F /. 1
= ((g2 | m) | pl) /. (w1 + 1) )
by A401, A402, A412;
then A415:
F /. 1 =
(g2 | m) /. (w1 + 1)
by A397
.=
G1 * mi,
K1
by A259, A260, A261, A262, MATRIX_1:def 8
;
[mi,K1] in Indices G1
by A26, A87, A259, A260, A261, ZFMISC_1:106;
then
(
j1 = mi &
j2 = K1 )
by A412, A415, GOBOARD1:21;
hence (abs (i1 - j1)) + (abs (i2 - j2)) =
(abs ((mi - 1) - mi)) + 0
by A414, ABSVALUE:7
.=
abs (- 1)
.=
abs 1
by COMPLEX1:138
.=
1
by ABSVALUE:def 1
;
:: thesis: verum end; set hf =
h1 ^ F;
A416:
now let i1,
i2,
j1,
j2 be
Element of
NAT ;
:: thesis: ( [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 A417:
(
[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 )
;
:: thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1then A418:
(
h2 /. 1
= G1 * (ma + 1),
K2 &
ma + 1
in dom G1 )
by A298, A302;
then
[(ma + 1),K2] in Indices G1
by A87, A277, A278, A279, ZFMISC_1:106;
then A419:
(
j1 = ma + 1 &
j2 = K2 )
by A417, A418, GOBOARD1:21;
A420:
(
len F in dom F &
0 <= 1 )
by A402, A403, FINSEQ_1:3;
A421:
(h1 ^ F) /. (len (h1 ^ F)) =
(h1 ^ F) /. ((len h1) + (len F))
by FINSEQ_1:35
.=
F /. (len F)
by A420, FINSEQ_4:84
.=
((g2 | m) | pl) /. (w1 + LL)
by A401, A402, A420
.=
G1 * ma,
K2
by A281, A397, A401, A402, A420
;
[ma,K2] in Indices G1
by A28, A87, A277, A278, A279, ZFMISC_1:106;
then
(
i1 = ma &
i2 = K2 )
by A417, A421, GOBOARD1:21;
hence (abs (i1 - j1)) + (abs (i2 - j2)) =
(abs (ma - (ma + 1))) + 0
by A419, ABSVALUE:7
.=
abs (- ((ma + 1) - ma))
.=
abs 1
by COMPLEX1:138
.=
1
by ABSVALUE:def 1
;
:: thesis: verum end; A422:
(h1 ^ F) ^ h2 is_sequence_on G1
proof
thus
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 A305, A407, GOBOARD1:39;
:: according to GOBOARD1:def 11 :: thesis: for b1 being Element of NAT holds
( not b1 in dom ((h1 ^ F) ^ h2) or not b1 + 1 in dom ((h1 ^ F) ^ h2) or for b2, b3, b4, b5 being Element of NAT holds
( not [b2,b3] in Indices G1 or not [b4,b5] in Indices G1 or not ((h1 ^ F) ^ h2) /. b1 = G1 * b2,b3 or not ((h1 ^ F) ^ h2) /. (b1 + 1) = G1 * b4,b5 or (abs (b2 - b4)) + (abs (b3 - b5)) = 1 ) )
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 A307, A409, A411, GOBOARD1:40;
hence
for
b1 being
Element of
NAT holds
( not
b1 in dom ((h1 ^ F) ^ h2) or not
b1 + 1
in dom ((h1 ^ F) ^ h2) or for
b2,
b3,
b4,
b5 being
Element of
NAT holds
( not
[b2,b3] in Indices G1 or not
[b4,b5] in Indices G1 or not
((h1 ^ F) ^ h2) /. b1 = G1 * b2,
b3 or not
((h1 ^ F) ^ h2) /. (b1 + 1) = G1 * b4,
b5 or
(abs (b2 - b4)) + (abs (b3 - b5)) = 1 ) )
by A310, A416, GOBOARD1:40;
:: thesis: verum
end; A423:
now per cases
( mi = 1 or mi <> 1 )
;
suppose A424:
mi = 1
;
:: thesis: ((h1 ^ F) ^ h2) /. 1 in rng (Line G1,1)then
h1 = {}
by A296;
then A425:
(h1 ^ F) ^ h2 = F ^ h2
by FINSEQ_1:47;
A426:
( 1
in Seg LL & 1
<= pf )
by A19, A251, A403, FINSEQ_1:3;
A427:
pf in Seg pl
by A254, A396, FINSEQ_1:3;
((h1 ^ F) ^ h2) /. 1 =
F /. 1
by A401, A402, A425, A426, FINSEQ_4:83
.=
((g2 | m) | pl) /. (w1 + 1)
by A401, A426
.=
(g2 | m) /. pf
by A252, A427, FINSEQ_4:86
;
hence
((h1 ^ F) ^ h2) /. 1
in rng (Line G1,1)
by A251, A424;
:: thesis: verum end; suppose A428:
mi <> 1
;
:: thesis: ((h1 ^ F) ^ h2) /. 1 in rng (Line G1,1)
1
<= mi
by A26, FINSEQ_3:27;
then
1
< mi
by A428, XXREAL_0:1;
then
1
+ 1
<= mi
by NAT_1:13;
then A429:
1
<= l1
by XREAL_1:21;
then A430:
1
in Seg l1
by FINSEQ_1:3;
A431:
len (h1 ^ F) = (len h1) + (len F)
by FINSEQ_1:35;
len (Line G1,1) = width G1
by MATRIX_1:def 8;
then A432:
K1 in dom L1
by A259, A260, A261, FINSEQ_1:def 3;
then A433:
L1 /. K1 = L1 . K1
by PARTFUN1:def 8;
0 <= len F
by NAT_1:2;
then
0 + 1
<= len (h1 ^ F)
by A296, A429, A431, XREAL_1:9;
then
1
in dom (h1 ^ F)
by FINSEQ_3:27;
then ((h1 ^ F) ^ h2) /. 1 =
(h1 ^ F) /. 1
by FINSEQ_4:83
.=
h1 /. 1
by A296, A297, A430, FINSEQ_4:83
.=
G1 * 1,
K1
by A296, A297, A430
.=
L1 /. K1
by A259, A260, A261, A433, MATRIX_1:def 8
;
hence
((h1 ^ F) ^ h2) /. 1
in rng (Line G1,1)
by A432, PARTFUN2:4;
:: thesis: verum A434:
len ((h1 ^ F) ^ h2) =
(len (h1 ^ F)) + (len h2)
by FINSEQ_1:35
.=
((len h1) + (len F)) + (len h2)
by FINSEQ_1:35
;
0 + 0 <= (len h1) + (len h2)
by NAT_1:2;
then A435:
0 + 1
<= (len F) + ((len h1) + (len h2))
by A403, XREAL_1:9;
A436:
now per cases
( ma = len G1 or ma <> len G1 )
;
suppose A437:
ma = len G1
;
:: thesis: ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line G1,(len G1))then
h2 = {}
by A298;
then A438:
(
(h1 ^ F) ^ h2 = h1 ^ F & 1
<= pl )
by A19, A252, FINSEQ_1:3, FINSEQ_1:47;
then A439:
(
len F in dom F &
pl in Seg pl )
by A403, FINSEQ_1:3, FINSEQ_3:27;
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) =
((h1 ^ F) ^ h2) /. ((len h1) + (len F))
by A438, FINSEQ_1:35
.=
F /. LL
by A401, A438, A439, FINSEQ_4:84
.=
((g2 | m) | pl) /. pl
by A401, A402, A408, A439
.=
(g2 | m) /. pl
by A252, A439, FINSEQ_4:86
;
hence
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line G1,(len G1))
by A252, A437;
:: thesis: verum end; suppose A440:
ma <> len G1
;
:: thesis: ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line G1,(len G1))
ma <= len G1
by A28, FINSEQ_3:27;
then
ma < len G1
by A440, XXREAL_0:1;
then
ma + 1
<= len G1
by NAT_1:13;
then A441:
1
<= l2
by XREAL_1:21;
then A442:
l2 in Seg l2
by FINSEQ_1:3;
len (Line G1,(len G1)) = width G1
by MATRIX_1:def 8;
then A443:
K2 in dom Ll
by A277, A278, A279, FINSEQ_1:def 3;
then A444:
Ll /. K2 = Ll . K2
by PARTFUN1:def 8;
A445:
len h2 in dom h2
by A298, A441, FINSEQ_3:27;
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) =
((h1 ^ F) ^ h2) /. ((len (h1 ^ F)) + (len h2))
by FINSEQ_1:35
.=
h2 /. l2
by A298, A445, FINSEQ_4:84
.=
G1 * (ma + l2),
K2
by A298, A299, A442
.=
Ll /. K2
by A277, A278, A279, A444, MATRIX_1:def 8
;
hence
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line G1,(len G1))
by A443, PARTFUN2:4;
:: thesis: verum end; A446:
rng ((h1 ^ F) ^ h2) =
(rng (h1 ^ F)) \/ (rng h2)
by FINSEQ_1:44
.=
((rng h1) \/ (rng F)) \/ (rng h2)
by FINSEQ_1:44
;
A447:
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
let k be
Element of
NAT ;
:: thesis: ( k in Seg (width G1) & (rng F) /\ (rng (Col G1,k)) = {} implies (rng ((h1 ^ F) ^ h2)) /\ (rng (Col G1,k)) = {} )
assume that A448:
k in Seg (width G1)
and A449:
(rng F) /\ (rng (Col G1,k)) = {}
;
:: thesis: (rng ((h1 ^ F) ^ h2)) /\ (rng (Col G1,k)) = {}
set gg =
Col G1,
k;
assume A450:
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col G1,k)) <> {}
;
:: thesis: contradiction
consider x being
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col G1,k));
rng ((h1 ^ F) ^ h2) = (rng F) \/ ((rng h1) \/ (rng h2))
by A446, XBOOLE_1:4;
then A451:
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col G1,k)) =
{} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col G1,k)))
by A449, XBOOLE_1:23
.=
((rng h1) /\ (rng (Col G1,k))) \/ ((rng h2) /\ (rng (Col G1,k)))
by XBOOLE_1:23
;
A452:
(
len (Col G1,K1) = len G1 &
len (Col G1,K2) = len G1 )
by MATRIX_1:def 9;
now per cases
( x in (rng h1) /\ (rng (Col G1,k)) or x in (rng h2) /\ (rng (Col G1,k)) )
by A450, A451, XBOOLE_0:def 3;
suppose
x in (rng h1) /\ (rng (Col G1,k))
;
:: thesis: contradictionthen A453:
(
x in rng h1 &
x in rng (Col G1,k) )
by XBOOLE_0:def 4;
then consider i being
Element of
NAT such that A454:
(
i in dom h1 &
x = h1 /. i )
by PARTFUN2:4;
A455:
x = G1 * i,
K1
by A296, A454;
reconsider y =
x as
Point of
(TOP-REAL 2) by A454;
A456:
dom CK1 =
Seg (len G1)
by A452, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
then A457:
i in dom CK1
by A300, A454;
A458:
(
Lmi /. K1 = Lmi . K1 &
CK1 /. mi = CK1 . mi )
by A26, A259, A456, PARTFUN1:def 8;
CK1 /. i = CK1 . i
by A300, A454, A456, PARTFUN1:def 8;
then
y = CK1 /. i
by A455, A456, A457, MATRIX_1:def 9;
then
y in rng CK1
by A457, PARTFUN2:4;
then A459:
(
K1 = k & 1
in Seg LL )
by A259, A260, A261, A403, A448, A453, FINSEQ_1:3, GOBOARD1:20;
then
(
F /. 1
= ((g2 | m) | pl) /. (w1 + 1) &
((g2 | m) | pl) /. (w1 + 1) = (g2 | m) /. (w1 + 1) )
by A397, A401;
then
F /. 1
= CK1 /. mi
by A26, A259, A260, A261, A458, GOBOARD1:17;
then
(
F /. 1
in rng (Col G1,k) &
F /. 1
in rng F )
by A26, A401, A402, A456, A459, PARTFUN2:4;
hence
contradiction
by A449, XBOOLE_0:def 4;
:: thesis: verum end; suppose
x in (rng h2) /\ (rng (Col G1,k))
;
:: thesis: contradictionthen A460:
(
x in rng h2 &
x in rng (Col G1,k) )
by XBOOLE_0:def 4;
then consider i being
Element of
NAT such that A461:
(
i in dom h2 &
x = h2 /. i )
by PARTFUN2:4;
A462:
x = G1 * (ma + i),
K2
by A298, A461;
reconsider y =
x as
Point of
(TOP-REAL 2) by A461;
A463:
dom CK2 =
Seg (len G1)
by A452, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
then A464:
ma + i in dom CK2
by A302, A461;
A465:
(
Lma /. K2 = Lma . K2 &
CK2 /. ma = CK2 . ma )
by A28, A277, A463, PARTFUN1:def 8;
CK2 /. (ma + i) = CK2 . (ma + i)
by A302, A461, A463, PARTFUN1:def 8;
then
y = CK2 /. (ma + i)
by A462, A463, A464, MATRIX_1:def 9;
then
y in rng CK2
by A464, PARTFUN2:4;
then A466:
K2 = k
by A277, A278, A279, A448, A460, GOBOARD1:20;
A467:
LL in Seg LL
by A403, FINSEQ_1:3;
then
(
F /. LL = ((g2 | m) | pl) /. (w1 + LL) &
((g2 | m) | pl) /. (w1 + LL) = (g2 | m) /. (w1 + LL) )
by A397, A401;
then
F /. LL = CK2 /. ma
by A28, A277, A278, A279, A465, GOBOARD1:17;
then
(
F /. LL in rng (Col G1,k) &
F /. LL in rng F )
by A28, A401, A402, A463, A466, A467, PARTFUN2:4;
hence
contradiction
by A449, XBOOLE_0:def 4;
:: thesis: verum end;
hence
contradiction
;
:: thesis: verum
end; A468:
(rng tt) /\ (rng ((h1 ^ F) ^ h2)) =
(((rng h1) \/ (rng F)) /\ (rng tt)) \/ {}
by A384, A446, XBOOLE_1:23
.=
{} \/ ((rng F) /\ (rng tt))
by A343, XBOOLE_1:23
.=
(rng tt) /\ (rng F)
;
rng tt c= rng f
by A245, A246, XBOOLE_1:1;
then A469:
rng tt c= rng g1
by A192, XBOOLE_1:1;
rng F c= rng g2
then A471:
(rng ((h1 ^ F) ^ h2)) /\ (rng tt) c= (rng g1) /\ (rng g2)
by A468, A469, XBOOLE_1:27;
A472:
( 1
in dom ((h1 ^ F) ^ h2) &
len ((h1 ^ F) ^ h2) in dom ((h1 ^ F) ^ h2) )
by A434, A435, FINSEQ_3:27;
(rng F) /\ (rng C) = {}
proof
assume A473:
not
(rng F) /\ (rng C) = {}
;
:: thesis: contradiction
consider x being
Element of
(rng F) /\ (rng C);
A474:
(
x in rng F &
x in rng C )
by A473, XBOOLE_0:def 4;
then consider i1 being
Element of
NAT such that A475:
(
i1 in dom F &
F /. i1 = x )
by PARTFUN2:4;
A476:
Seg (len F) = dom F
by FINSEQ_1:def 3;
then A477:
(
F /. i1 = ((g2 | m) | pl) /. (w1 + i1) &
w1 is
Element of
NAT &
((g2 | m) | pl) /. (w1 + i1) = (g2 | m) /. (w1 + i1) &
w1 + i1 in dom (g2 | m) )
by A397, A401, A475;
reconsider w =
w1 as
Element of
NAT ;
(
g2 /. (w + i1) in rng C &
w + i1 in dom g2 )
by A8, A19, A35, A474, A475, A477, FINSEQ_4:86;
then A478:
(
m <= w + i1 &
i1 <= LL )
by A8, A401, A475, A476, FINSEQ_1:3;
then
w + i1 <= w + LL
by XREAL_1:9;
hence
contradiction
by A35, A295, A478, XXREAL_0:2;
:: thesis: verum
end; then
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col G1,(width G1))) = {}
by A15, A447;
then
rng ((h1 ^ F) ^ h2) misses rng (Col G1,(width G1))
by XBOOLE_0:def 7;
then A479:
(
(h1 ^ F) ^ h2 is_sequence_on DelCol G1,
(width G1) &
((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 A15, A16, A17, A195, A196, A422, A423, A436, A472, GOBOARD1:37, GOBOARD1:41;
width (DelCol G1,(width G1)) = k
by A5, A15, A67, GOBOARD1:26, NAT_1:3;
then A480:
(rng ((h1 ^ F) ^ h2)) /\ (rng tt) <> {}
by A4, A68, A246, A434, A435, A479;
consider x being
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng tt);
x in (rng ((h1 ^ F) ^ h2)) /\ (rng tt)
by A480;
hence
(rng g1) /\ (rng g2) <> {}
by A471;
:: thesis: verum end; suppose A481:
pl < pf
;
:: thesis: (rng g1) /\ (rng g2) <> {} set F1 =
(g2 | m) | pf;
(
pl <= pf &
pf <= pf + 1 )
by A481, NAT_1:11;
then reconsider LL =
(pf + 1) - pl as
Element of
NAT by INT_1:18, XXREAL_0:2;
A482:
for
n being
Element of
NAT st
n in Seg LL holds
(pf + 1) - n is
Element of
NAT
A484:
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 ;
:: thesis: ( n in Seg LL & k = (pf + 1) - n implies ( ((g2 | m) | pf) /. k = (g2 | m) /. k & k in dom (g2 | m) ) )
assume that A485:
n in Seg LL
and A486:
k = (pf + 1) - n
;
:: thesis: ( ((g2 | m) | pf) /. k = (g2 | m) /. k & k in dom (g2 | m) )
A487:
( 1
<= n &
n <= LL &
0 <= pl )
by A485, FINSEQ_1:3, NAT_1:2;
then
LL <= (pf + 1) - 0
by XREAL_1:15;
then reconsider w =
(pf + 1) - n as
Element of
NAT by A487, INT_1:18, XXREAL_0:2;
A488:
(
(pf + 1) - n <= (pf + 1) - 1 &
(pf + 1) - LL <= (pf + 1) - n )
by A487, XREAL_1:15;
then
1
<= (pf + 1) - n
by A254, XXREAL_0:2;
then
w in Seg pf
by A488, FINSEQ_1:3;
hence
(
((g2 | m) | pf) /. k = (g2 | m) /. k &
k in dom (g2 | m) )
by A251, A486, FINSEQ_4:86;
:: thesis: verum
end; 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;
A489:
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 A491:
(
len F = LL & ( for
n being
Nat st
n in Seg LL holds
S11[
n,
F /. n] ) )
from FINSEQ_4:sch 1(A489);
A492:
Seg (len F) = dom F
by FINSEQ_1:def 3;
set FF =
(h1 ^ F) ^ h2;
(
pl + 1
<= pf &
pf <= pf + 1 )
by A481, NAT_1:13;
then
(
pl + 1
<= pf + 1 &
dom F = dom F )
by XXREAL_0:2;
then A493:
( 1
<= LL &
len F = LL )
by A491, XREAL_1:21;
now let n be
Element of
NAT ;
:: thesis: ( n in dom F implies ex i, j being Element of NAT st
( [i,j] in Indices G1 & F /. n = G1 * i,j ) )assume A494:
n in dom F
;
:: thesis: 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 A482, A491, A492;
A495:
(
n in Seg LL &
dom F = Seg LL &
F /. n = ((g2 | m) | pf) /. w )
by A491, A492, A494;
then
(
(pf + 1) - n is
Element of
NAT &
(pf + 1) - n in dom (g2 | m) &
F /. n = (g2 | m) /. w )
by A484;
then consider i,
j being
Element of
NAT such that A496:
(
[i,j] in Indices G1 &
(g2 | m) /. w = G1 * i,
j )
by A10, GOBOARD1:def 11;
take i =
i;
:: thesis: ex j being Element of NAT st
( [i,j] in Indices G1 & F /. n = G1 * i,j )take j =
j;
:: thesis: ( [i,j] in Indices G1 & F /. n = G1 * i,j )thus
(
[i,j] in Indices G1 &
F /. n = G1 * i,
j )
by A484, A495, A496;
:: thesis: 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 A303, GOBOARD1:39;
then A497:
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 A305, GOBOARD1:39;
A498:
now let n be
Element of
NAT ;
:: thesis: ( 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 A499:
(
n in dom F &
n + 1
in dom F )
;
:: thesis: 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))then reconsider w3 =
(pf + 1) - n,
w2 =
(pf + 1) - (n + 1) as
Element of
NAT by A482, A491, A492;
(
n in Seg LL &
n + 1
in Seg LL &
dom F = Seg LL &
F /. n = ((g2 | m) | pf) /. w3 &
F /. (n + 1) = ((g2 | m) | pf) /. w2 &
(pf + 1) - (n + 1) = ((pf + 1) - n) - 1 )
by A491, A492, A499;
then A500:
(
(pf + 1) - n in dom (g2 | m) &
F /. n = (g2 | m) /. w3 &
(pf + 1) - (n + 1) in dom (g2 | m) &
F /. (n + 1) = (g2 | m) /. w2 )
by A484;
A501:
w2 + 1
= (pf + 1) - n
;
let i1,
i2,
j1,
j2 be
Element of
NAT ;
:: thesis: ( [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
(
[i1,i2] in Indices G1 &
[j1,j2] in Indices G1 &
F /. n = G1 * i1,
i2 &
F /. (n + 1) = G1 * j1,
j2 )
;
:: thesis: 1 = (abs (i1 - j1)) + (abs (i2 - j2))hence 1 =
(abs (j1 - i1)) + (abs (j2 - i2))
by A10, A500, A501, GOBOARD1:def 11
.=
(abs (- (i1 - j1))) + (abs (- (i2 - j2)))
.=
(abs (i1 - j1)) + (abs (- (i2 - j2)))
by COMPLEX1:138
.=
(abs (i1 - j1)) + (abs (i2 - j2))
by COMPLEX1:138
;
:: thesis: verum end; A502:
(pf + 1) - 1
= pf
;
now let i1,
i2,
j1,
j2 be
Element of
NAT ;
:: thesis: ( [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 A503:
(
[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 )
;
:: thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1then A504:
(
h1 /. (len h1) = G1 * l1,
K1 &
l1 in dom G1 )
by A296, A300;
then
[l1,K1] in Indices G1
by A87, A259, A260, A261, ZFMISC_1:106;
then A505:
(
i1 = l1 &
i2 = K1 &
0 <= 1 )
by A503, A504, GOBOARD1:21;
reconsider w4 =
(pf + 1) - 1 as
Element of
NAT ;
A506:
F /. 1 =
((g2 | m) | pf) /. w4
by A491, A492, A503
.=
(g2 | m) /. w4
by A484, A491, A492, A503
.=
G1 * mi,
K1
by A259, A260, A261, A262, MATRIX_1:def 8
;
[mi,K1] in Indices G1
by A26, A87, A259, A260, A261, ZFMISC_1:106;
then
(
j1 = mi &
j2 = K1 )
by A503, A506, GOBOARD1:21;
hence (abs (i1 - j1)) + (abs (i2 - j2)) =
(abs ((mi - 1) - mi)) + 0
by A505, ABSVALUE:7
.=
abs (- 1)
.=
abs 1
by COMPLEX1:138
.=
1
by ABSVALUE:def 1
;
:: thesis: verum end; then A507:
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 A307, A498, GOBOARD1:40;
set hf =
h1 ^ F;
now let i1,
i2,
j1,
j2 be
Element of
NAT ;
:: thesis: ( [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 A508:
(
[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 )
;
:: thesis: (abs (i1 - j1)) + (abs (i2 - j2)) = 1then A509:
(
h2 /. 1
= G1 * (ma + 1),
K2 &
ma + 1
in dom G1 )
by A298, A302;
then
[(ma + 1),K2] in Indices G1
by A87, A277, A278, A279, ZFMISC_1:106;
then A510:
(
j1 = ma + 1 &
j2 = K2 )
by A508, A509, GOBOARD1:21;
A511:
(
len F in dom F &
0 <= 1 )
by A493, FINSEQ_3:27;
reconsider u =
(pf + 1) - LL as
Element of
NAT ;
A512:
(h1 ^ F) /. (len (h1 ^ F)) =
(h1 ^ F) /. ((len h1) + (len F))
by FINSEQ_1:35
.=
F /. (len F)
by A511, FINSEQ_4:84
.=
((g2 | m) | pf) /. u
by A491, A492, A511
.=
(g2 | m) /. u
by A484, A491, A492, A511
.=
G1 * ma,
K2
by A277, A278, A279, A280, MATRIX_1:def 8
;
[ma,K2] in Indices G1
by A28, A87, A277, A278, A279, ZFMISC_1:106;
then
(
i1 = ma &
i2 = K2 )
by A508, A512, GOBOARD1:21;
hence (abs (i1 - j1)) + (abs (i2 - j2)) =
(abs (ma - (ma + 1))) + 0
by A510, ABSVALUE:7
.=
abs (- ((ma + 1) - ma))
.=
abs 1
by COMPLEX1:138
.=
1
by ABSVALUE:def 1
;
:: thesis: verum end; 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 A310, A507, GOBOARD1:40;
then A513:
(h1 ^ F) ^ h2 is_sequence_on G1
by A497, GOBOARD1:def 11;
A514:
now per cases
( mi = 1 or mi <> 1 )
;
suppose A515:
mi = 1
;
:: thesis: ((h1 ^ F) ^ h2) /. 1 in rng (Line G1,1)then
h1 = {}
by A296;
then A516:
(h1 ^ F) ^ h2 = F ^ h2
by FINSEQ_1:47;
A517:
( 1
in Seg LL & 1
<= pl )
by A19, A252, A493, FINSEQ_1:3;
A518:
pf in Seg pf
by A254, FINSEQ_1:3;
((h1 ^ F) ^ h2) /. 1 =
F /. 1
by A491, A492, A516, A517, FINSEQ_4:83
.=
((g2 | m) | pf) /. pf
by A491, A502, A517
.=
(g2 | m) /. pf
by A251, A518, FINSEQ_4:86
;
hence
((h1 ^ F) ^ h2) /. 1
in rng (Line G1,1)
by A251, A515;
:: thesis: verum end; suppose A519:
mi <> 1
;
:: thesis: ((h1 ^ F) ^ h2) /. 1 in rng (Line G1,1)
1
<= mi
by A26, FINSEQ_3:27;
then
1
< mi
by A519, XXREAL_0:1;
then
1
+ 1
<= mi
by NAT_1:13;
then A520:
1
<= l1
by XREAL_1:21;
then A521:
1
in Seg l1
by FINSEQ_1:3;
A522:
len (h1 ^ F) = (len h1) + (len F)
by FINSEQ_1:35;
len (Line G1,1) = width G1
by MATRIX_1:def 8;
then A523:
K1 in dom L1
by A259, A260, A261, FINSEQ_1:def 3;
then A524:
L1 /. K1 = L1 . K1
by PARTFUN1:def 8;
0 <= len F
by NAT_1:2;
then
0 + 1
<= len (h1 ^ F)
by A296, A520, A522, XREAL_1:9;
then
1
in dom (h1 ^ F)
by FINSEQ_3:27;
then ((h1 ^ F) ^ h2) /. 1 =
(h1 ^ F) /. 1
by FINSEQ_4:83
.=
h1 /. 1
by A296, A297, A521, FINSEQ_4:83
.=
G1 * 1,
K1
by A296, A297, A521
.=
L1 /. K1
by A259, A260, A261, A524, MATRIX_1:def 8
;
hence
((h1 ^ F) ^ h2) /. 1
in rng (Line G1,1)
by A523, PARTFUN2:4;
:: thesis: verum A525:
len ((h1 ^ F) ^ h2) =
(len (h1 ^ F)) + (len h2)
by FINSEQ_1:35
.=
((len h1) + (len F)) + (len h2)
by FINSEQ_1:35
;
0 + 0 <= (len h1) + (len h2)
by NAT_1:2;
then A526:
0 + 1
<= (len F) + ((len h1) + (len h2))
by A493, XREAL_1:9;
A527:
now per cases
( ma = len G1 or ma <> len G1 )
;
suppose A528:
ma = len G1
;
:: thesis: ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line G1,(len G1))then
h2 = {}
by A298;
then A529:
(h1 ^ F) ^ h2 = h1 ^ F
by FINSEQ_1:47;
A530:
(pf + 1) - ((pf + 1) - pl) = pl
;
A531:
(
len F in dom F &
pl in Seg pf )
by A254, A481, A493, FINSEQ_1:3, FINSEQ_3:27;
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) =
((h1 ^ F) ^ h2) /. ((len h1) + (len F))
by A529, FINSEQ_1:35
.=
F /. LL
by A491, A529, A531, FINSEQ_4:84
.=
((g2 | m) | pf) /. pl
by A491, A492, A530, A531
.=
(g2 | m) /. pl
by A251, A531, FINSEQ_4:86
;
hence
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line G1,(len G1))
by A252, A528;
:: thesis: verum end; suppose A532:
ma <> len G1
;
:: thesis: ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line G1,(len G1))
ma <= len G1
by A28, FINSEQ_3:27;
then
ma < len G1
by A532, XXREAL_0:1;
then
ma + 1
<= len G1
by NAT_1:13;
then A533:
1
<= l2
by XREAL_1:21;
then A534:
l2 in Seg l2
by FINSEQ_1:3;
len (Line G1,(len G1)) = width G1
by MATRIX_1:def 8;
then A535:
K2 in dom Ll
by A277, A278, A279, FINSEQ_1:def 3;
then A536:
Ll /. K2 = Ll . K2
by PARTFUN1:def 8;
A537:
len h2 in dom h2
by A298, A533, FINSEQ_3:27;
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) =
((h1 ^ F) ^ h2) /. ((len (h1 ^ F)) + (len h2))
by FINSEQ_1:35
.=
h2 /. l2
by A298, A537, FINSEQ_4:84
.=
G1 * (ma + l2),
K2
by A298, A299, A534
.=
Ll /. K2
by A277, A278, A279, A536, MATRIX_1:def 8
;
hence
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line G1,(len G1))
by A535, PARTFUN2:4;
:: thesis: verum end; A538:
rng ((h1 ^ F) ^ h2) =
(rng (h1 ^ F)) \/ (rng h2)
by FINSEQ_1:44
.=
((rng h1) \/ (rng F)) \/ (rng h2)
by FINSEQ_1:44
;
A539:
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
let k be
Element of
NAT ;
:: thesis: ( k in Seg (width G1) & (rng F) /\ (rng (Col G1,k)) = {} implies (rng ((h1 ^ F) ^ h2)) /\ (rng (Col G1,k)) = {} )
assume that A540:
k in Seg (width G1)
and A541:
(rng F) /\ (rng (Col G1,k)) = {}
;
:: thesis: (rng ((h1 ^ F) ^ h2)) /\ (rng (Col G1,k)) = {}
set gg =
Col G1,
k;
assume A542:
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col G1,k)) <> {}
;
:: thesis: contradiction
consider x being
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col G1,k));
rng ((h1 ^ F) ^ h2) = (rng F) \/ ((rng h1) \/ (rng h2))
by A538, XBOOLE_1:4;
then A543:
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col G1,k)) =
{} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col G1,k)))
by A541, XBOOLE_1:23
.=
((rng h1) /\ (rng (Col G1,k))) \/ ((rng h2) /\ (rng (Col G1,k)))
by XBOOLE_1:23
;
A544:
(
len (Col G1,K1) = len G1 &
len (Col G1,K2) = len G1 )
by MATRIX_1:def 9;
now per cases
( x in (rng h1) /\ (rng (Col G1,k)) or x in (rng h2) /\ (rng (Col G1,k)) )
by A542, A543, XBOOLE_0:def 3;
suppose
x in (rng h1) /\ (rng (Col G1,k))
;
:: thesis: contradictionthen A545:
(
x in rng h1 &
x in rng (Col G1,k) )
by XBOOLE_0:def 4;
then consider i being
Element of
NAT such that A546:
(
i in dom h1 &
x = h1 /. i )
by PARTFUN2:4;
A547:
x = G1 * i,
K1
by A296, A546;
reconsider y =
x as
Point of
(TOP-REAL 2) by A546;
A548:
(pf + 1) - 1
= pf
;
A549:
dom CK1 =
Seg (len G1)
by A544, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
then A550:
i in dom CK1
by A300, A546;
A551:
(
Lmi /. K1 = Lmi . K1 &
CK1 /. mi = CK1 . mi )
by A26, A259, A549, PARTFUN1:def 8;
CK1 /. i = CK1 . i
by A300, A546, A549, PARTFUN1:def 8;
then
y = CK1 /. i
by A547, A549, A550, MATRIX_1:def 9;
then
y in rng CK1
by A550, PARTFUN2:4;
then A552:
(
K1 = k & 1
in Seg LL )
by A259, A260, A261, A493, A540, A545, FINSEQ_1:3, GOBOARD1:20;
then
(
F /. 1
= ((g2 | m) | pf) /. pf &
((g2 | m) | pf) /. pf = (g2 | m) /. pf )
by A484, A491, A548;
then
F /. 1
= CK1 /. mi
by A26, A259, A260, A261, A551, GOBOARD1:17;
then
(
F /. 1
in rng (Col G1,k) &
F /. 1
in rng F )
by A26, A491, A492, A549, A552, PARTFUN2:4;
hence
contradiction
by A541, XBOOLE_0:def 4;
:: thesis: verum end; suppose
x in (rng h2) /\ (rng (Col G1,k))
;
:: thesis: contradictionthen A553:
(
x in rng h2 &
x in rng (Col G1,k) )
by XBOOLE_0:def 4;
then consider i being
Element of
NAT such that A554:
(
i in dom h2 &
x = h2 /. i )
by PARTFUN2:4;
A555:
x = G1 * (ma + i),
K2
by A298, A554;
reconsider y =
x as
Point of
(TOP-REAL 2) by A554;
A556:
LL in Seg LL
by A493, FINSEQ_1:3;
reconsider u =
(pf + 1) - LL as
Element of
NAT ;
A557:
dom CK2 =
Seg (len G1)
by A544, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
then A558:
ma + i in dom CK2
by A302, A554;
A559:
(
Lma /. K2 = Lma . K2 &
CK2 /. ma = CK2 . ma )
by A28, A277, A557, PARTFUN1:def 8;
CK2 /. (ma + i) = CK2 . (ma + i)
by A302, A554, A557, PARTFUN1:def 8;
then
y = CK2 /. (ma + i)
by A555, A557, A558, MATRIX_1:def 9;
then
y in rng CK2
by A558, PARTFUN2:4;
then A560:
K2 = k
by A277, A278, A279, A540, A553, GOBOARD1:20;
(
F /. LL = ((g2 | m) | pf) /. u &
((g2 | m) | pf) /. u = (g2 | m) /. u )
by A484, A491, A556;
then
F /. LL = CK2 /. ma
by A28, A277, A278, A279, A559, GOBOARD1:17;
then
(
F /. LL in rng (Col G1,k) &
F /. LL in rng F )
by A28, A491, A492, A556, A557, A560, PARTFUN2:4;
hence
contradiction
by A541, XBOOLE_0:def 4;
:: thesis: verum end;
hence
contradiction
;
:: thesis: verum
end; A561:
(rng tt) /\ (rng ((h1 ^ F) ^ h2)) =
(((rng h1) \/ (rng F)) /\ (rng tt)) \/ {}
by A384, A538, XBOOLE_1:23
.=
{} \/ ((rng F) /\ (rng tt))
by A343, XBOOLE_1:23
.=
(rng tt) /\ (rng F)
;
rng tt c= rng f
by A245, A246, XBOOLE_1:1;
then A562:
rng tt c= rng g1
by A192, XBOOLE_1:1;
rng F c= rng g2
then A564:
(rng ((h1 ^ F) ^ h2)) /\ (rng tt) c= (rng g1) /\ (rng g2)
by A561, A562, XBOOLE_1:27;
A565:
( 1
in dom ((h1 ^ F) ^ h2) &
len ((h1 ^ F) ^ h2) in dom ((h1 ^ F) ^ h2) )
by A525, A526, FINSEQ_3:27;
(rng F) /\ (rng C) = {}
proof
assume A566:
not
(rng F) /\ (rng C) = {}
;
:: thesis: contradiction
consider x being
Element of
(rng F) /\ (rng C);
A567:
(
x in rng F &
x in rng C )
by A566, XBOOLE_0:def 4;
then consider i1 being
Element of
NAT such that A568:
(
i1 in dom F &
F /. i1 = x )
by PARTFUN2:4;
reconsider w =
(pf + 1) - i1 as
Element of
NAT by A482, A491, A492, A568;
A569:
(
F /. i1 = ((g2 | m) | pf) /. w &
((g2 | m) | pf) /. w = (g2 | m) /. w &
w in dom (g2 | m) )
by A484, A491, A492, A568;
( 1
<= i1 &
i1 <= LL )
by A491, A568, FINSEQ_3:27;
then A570:
(
w <= (pf + 1) - 1 &
(pf + 1) - LL <= w )
by XREAL_1:15;
A571:
w in dom g2
by A8, A19, A35, A569, FINSEQ_4:86;
g2 /. w in rng C
by A8, A19, A35, A567, A568, A569, FINSEQ_4:86;
then
(
m <= w &
w < m )
by A8, A35, A276, A570, A571, XXREAL_0:2;
hence
contradiction
;
:: thesis: verum
end; then
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col G1,(width G1))) = {}
by A15, A539;
then
rng ((h1 ^ F) ^ h2) misses rng (Col G1,(width G1))
by XBOOLE_0:def 7;
then A572:
(
(h1 ^ F) ^ h2 is_sequence_on DelCol G1,
(width G1) &
((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 A15, A16, A17, A195, A196, A513, A514, A527, A565, GOBOARD1:37, GOBOARD1:41;
width (DelCol G1,(width G1)) = k
by A5, A15, A67, GOBOARD1:26, NAT_1:3;
then A573:
(rng ((h1 ^ F) ^ h2)) /\ (rng tt) <> {}
by A4, A68, A246, A525, A526, A572;
consider x being
Element of
(rng ((h1 ^ F) ^ h2)) /\ (rng tt);
x in (rng ((h1 ^ F) ^ h2)) /\ (rng tt)
by A573;
hence
(rng g1) /\ (rng g2) <> {}
by A564;
:: thesis: verum end; hence
(rng g1) /\ (rng g2) <> {}
;
:: thesis: verum end; hence
(rng g1) /\ (rng g2) <> {}
;
:: thesis: verum end;
end; end; hence
(rng g1) /\ (rng g2) <> {}
;
:: thesis: verum end;
hence
(rng g1) /\ (rng g2) <> {}
;
:: thesis: verum
end;
A574:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A2, A3);
A575:
now let k be
Element of
NAT ;
:: thesis: 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;
:: thesis: 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);
:: thesis: ( 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)) )
;
:: thesis: rng g1 meets rng g2then
(rng g1) /\ (rng g2) <> {}
by A574;
hence
rng g1 meets rng g2
by XBOOLE_0:def 7;
:: thesis: verum end;
width G <> 0
by GOBOARD1:def 5;
then
width G > 0
by NAT_1:3;
hence
rng f1 meets rng f2
by A1, A575; :: thesis: verum