( m in dom g2 implies g2 /. 1 = (g2 | m) /. 1 ) by FINSEQ_4:92;
then consider i being Nat such that
A35: i in dom (Col (G1,1)) and
A36: (g2 | m) /. 1 = (Col (G1,1)) . i by A10, A13, FINSEQ_2:10;
reconsider i = i as Nat ;
take i ; :: thesis:
i in Seg (len (Col (G1,1))) by A35, FINSEQ_1:def 3;
then i in Seg (len G1) by MATRIX_0:def 8;
hence i in dom G1 by FINSEQ_1:def 3; :: thesis:
then A37: (g2 | m) /. 1 = (Line (G1,i)) . 1 by A31, A36, MATRIX_0:42;
A38: (g2 | m) /. 1 in rng (g2 | m) by A33, PARTFUN2:2;
len (Line (G1,i)) = width G1 by MATRIX_0:def 7;
then dom (Line (G1,i)) = Seg (width G1) by FINSEQ_1:def 3;
then (g2 | m) /. 1 in rng (Line (G1,i)) by A31, A37, FUNCT_1:def 3;
hence (rng (g2 | m)) /\ (rng (Line (G1,i))) <> {} by A38, XBOOLE_0:def 4; :: thesis:

end;

consider mi being Nat such that
A39: ( S₃[mi] & ( for n being Nat st S₃[n] holds
mi <= n ) ) from NAT_1:sch 5(A34);
A40: ex n being Nat st S₃[n] by A34;
consider ma being Nat such that
A41: ( S₃[ma] & ( for n being Nat st S₃[n] holds
n <= ma ) ) from NAT_1:sch 6(A29, A40);
reconsider mi = mi, ma = ma as Nat ;
A42: 1 <= mi by A39, FINSEQ_3:25;
reconsider Lmi = Line (G1,mi) as FinSequence of (TOP-REAL 2) ;
defpred S₄[ Nat] means ( $1 in dom g1 & g1 /. $1 in rng (Line (G1,mi)) );
A43: for n being Nat st S₄[n] holds
n <= len g1 by FINSEQ_3:25;
A44: mi <= len G1 by A39, FINSEQ_3:25;
then ex n being Nat st S₄[n] by A4, A6, A8, A9, A42, GOBOARD1:29;
then A45: ex n being Nat st S₄[n] ;
consider ma1 being Nat such that
A46: ( S₄[ma1] & ( for n being Nat st S₄[n] holds
n <= ma1 ) ) from NAT_1:sch 6(A43, A45);
A47: ma <= len G1 by A41, FINSEQ_3:25;
1 <= mi by A39, FINSEQ_3:25;
then reconsider l1 = mi - 1, l2 = (len G1) - ma as Element of NAT by A47, INT_1:5;
A48: ma <= len G1 by A41, FINSEQ_3:25;
reconsider ma1 = ma1 as Nat ;
consider k1 being Element of NAT such that
A49: k1 in dom Lmi and
A50: g1 /. ma1 = Lmi /. k1 by A46, PARTFUN2:2;
Seg (len Lmi) = dom Lmi by FINSEQ_1:def 3;
then A51: k1 in Seg (width G1) by A49, MATRIX_0:def 7;
A52: dom G1 = Seg (len G1) by FINSEQ_1:def 3;
A53: ( mi = ma implies (rng g1) /\ (rng g2) <> {} )

consider n being Nat such that
A54: n in dom g1 and
A55: g1 /. n in rng (Line (G1,mi)) by A4, A6, A8, A9, A42, A44, GOBOARD1:29;
consider i being Element of NAT such that
A56: i in dom (Line (G1,mi)) and
A57: g1 /. n = Lmi /. i by A55, PARTFUN2:2;
A58: 1 <= i by A56, FINSEQ_3:25;
A59: len (Line (G1,mi)) = width G1 by MATRIX_0:def 7;
then i <= width G1 by A56, FINSEQ_3:25;
then consider m being Nat such that
A60: m in dom (g2 | m) and
A61: (g2 | m) /. m in rng (Col (G1,i)) by A32, A15, A14, A28, A58, GOBOARD1:33;
A62: (g2 | m) /. m in rng (g2 | m) by A60, PARTFUN2:2;
reconsider Ci = Col (G1,i) as FinSequence of (TOP-REAL 2) ;
A63: len (Col (G1,i)) = len G1 by MATRIX_0:def 8;
then A64: dom (Col (G1,i)) = Seg (len G1) by FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3 ;
assume A65: mi = ma ; :: thesis:
A66: dom (Line (G1,mi)) = Seg (len (Line (G1,mi))) by FINSEQ_1:def 3;
consider j being Element of NAT such that
A67: j in dom Ci and
A68: (g2 | m) /. m = Ci /. j by A61, PARTFUN2:2;
reconsider Lj = Line (G1,j) as FinSequence of (TOP-REAL 2) ;
len (Line (G1,mi)) = width G1 by MATRIX_0:def 7
.= len Lj by MATRIX_0:def 7 ;
then A69: dom (Line (G1,mi)) = dom Lj by A66, FINSEQ_1:def 3;
A70: (g2 | m) /. m = Ci . j by A67, A68, PARTFUN1:def 6
.= Lj . i by A56, A66, A59, A64, A67, MATRIX_0:42
.= Lj /. i by A56, A69, PARTFUN1:def 6 ;
len Lj = width G1 by MATRIX_0:def 7;
then i in dom Lj by A56, A66, A59, FINSEQ_1:def 3;
then (g2 | m) /. m in rng Lj by A70, PARTFUN2:2;
then A71: ( dom Ci = Seg (len Ci) & (rng (g2 | m)) /\ (rng (Line (G1,j))) <> {} ) by A62, FINSEQ_1:def 3, XBOOLE_0:def 4;

A72: now :: thesis:

assume j <> mi ; :: thesis:
then ( j < mi or j > mi ) by XXREAL_0:1;
hence contradiction by A39, A52, A41, A65, A63, A67, A71; :: thesis:

end;

g1 /. n in rng g1 by A54, PARTFUN2:2;
hence (rng g1) /\ (rng g2) <> {} by A18, A57, A62, A70, A72, XBOOLE_0:def 4; :: thesis:

end;

A73: width G1 in Seg (width G1) by A30, FINSEQ_1:1;
deffunc H₁( Nat) -> Element of the U1 of (TOP-REAL 2) = G1 * ($1,k1);
reconsider Ck1 = Col (G1,k1) as FinSequence of (TOP-REAL 2) ;
consider h1 being FinSequence of (TOP-REAL 2) such that
A74: ( len h1 = l1 & ( for n being Nat st n in dom h1 holds
h1 /. n = H₁(n) ) ) from FINSEQ_4:sch 2();
A75: dom g1 = Seg (len g1) by FINSEQ_1:def 3;

suppose A76: k = 0 ; :: thesis:

reconsider c1 = Col (G1,1) as FinSequence of (TOP-REAL 2) ;
consider x being Element of NAT such that
A77: x in dom c1 and
A78: g2 /. 1 = c1 /. x by A10, PARTFUN2:2;
reconsider lx = Line (G1,x) as FinSequence of (TOP-REAL 2) ;
A79: 1 <= x by A77, FINSEQ_3:25;
A80: len c1 = len G1 by MATRIX_0:def 8;
then x <= len G1 by A77, FINSEQ_3:25;
then consider m being Nat such that
A81: m in dom g1 and
A82: g1 /. m in rng lx by A4, A6, A8, A9, A79, GOBOARD1:29;
A83: g1 /. m in rng g1 by A81, PARTFUN2:2;
Seg (len c1) = dom c1 by FINSEQ_1:def 3;
then A84: x in dom G1 by A77, A80, FINSEQ_1:def 3;
A85: c1 /. x = c1 . x by A77, PARTFUN1:def 6;
consider y being Element of NAT such that
A86: y in dom lx and
A87: lx /. y = g1 /. m by A82, PARTFUN2:2;
( Seg (len lx) = dom lx & len lx = width G1 ) by FINSEQ_1:def 3, MATRIX_0:def 7;
then A88: y = 1 by A3, A76, A86, FINSEQ_1:2, TARSKI:def 1;
0 <> width G1 by MATRIX_0:def 10;
then 0 + 1 <= width G1 by NAT_1:14;
then A89: 1 in Seg (width G1) by FINSEQ_1:1;
1 in dom g2 by A5, FINSEQ_3:25;
then A90: g2 /. 1 in rng g2 by PARTFUN2:2;
lx /. y = lx . y by A86, PARTFUN1:def 6;
then g1 /. m = g2 /. 1 by A78, A89, A84, A87, A85, A88, MATRIX_0:42;
hence (rng g1) /\ (rng g2) <> {} by A83, A90, XBOOLE_0:def 4; :: thesis:

end;

suppose A91: k <> 0 ; :: thesis:

then A92: 0 < k ;
then A93: width G1 > 1 + 0 by A3, XREAL_1:8;
then A94: width G1 in Seg (width G1) by FINSEQ_1:1;

suppose mi = ma ; :: thesis:

hence (rng g1) /\ (rng g2) <> {} by A53; :: thesis:

end;

suppose A95: mi <> ma ; :: thesis:

1 <= ma1 by A46, FINSEQ_3:25;
then reconsider w = ma1 - 1 as Element of NAT by INT_1:5;
reconsider Lma = Line (G1,ma) as FinSequence of (TOP-REAL 2) ;
A96: Indices G1 = [:(dom G1),(Seg (width G1)):] by MATRIX_0:def 4;

A97: now :: thesis:

let n be Nat; :: thesis:
A98: l1 <= mi by XREAL_1:43;
assume A99: n in dom h1 ; :: thesis:
then A100: 1 <= n by FINSEQ_3:25;
n <= l1 by A74, A99, FINSEQ_3:25;
then A101: n <= mi by A98, XXREAL_0:2;
mi <= len G1 by A39, FINSEQ_3:25;
then n <= len G1 by A101, XXREAL_0:2;
hence n in dom G1 by A100, FINSEQ_3:25; :: thesis:

end;

A102: now :: thesis:

let n be Nat; :: thesis:
assume that
A103: n in dom h1 and
A104: n + 1 in dom h1 ; :: thesis:
n + 1 in dom G1 by A97, A104;
then A105: [(n + 1),k1] in Indices G1 by A51, A96, ZFMISC_1:87;
let i1, i2, j1, j2 be Nat; :: thesis:
assume that
A106: [i1,i2] in Indices G1 and
A107: [j1,j2] in Indices G1 and
A108: h1 /. n = G1 * (i1,i2) and
A109: h1 /. (n + 1) = G1 * (j1,j2) ; :: thesis:
h1 /. (n + 1) = G1 * ((n + 1),k1) by A74, A104;
then A110: ( j1 = n + 1 & j2 = k1 ) by A105, A107, A109, GOBOARD1:5;
n in dom G1 by A97, A103;
then A111: [n,k1] in Indices G1 by A51, A96, ZFMISC_1:87;
h1 /. n = G1 * (n,k1) by A74, A103;
then ( i1 = n & i2 = k1 ) by A111, A106, A108, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| = |.((n - n) + (- 1)).| + 0 by A110, ABSVALUE:2
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

A112: (rng h1) /\ (rng (g2 | m)) = {}

set x = the Element of (rng h1) /\ (rng (g2 | m));
assume A113: not (rng h1) /\ (rng (g2 | m)) = {} ; :: thesis:
then the Element of (rng h1) /\ (rng (g2 | m)) in rng h1 by XBOOLE_0:def 4;
then consider n1 being Element of NAT such that
A114: n1 in dom h1 and
A115: the Element of (rng h1) /\ (rng (g2 | m)) = h1 /. n1 by PARTFUN2:2;
A116: n1 <= l1 by A74, A114, FINSEQ_3:25;
n1 in dom G1 by A97, A114;
then A117: [n1,k1] in Indices G1 by A51, A96, ZFMISC_1:87;
the Element of (rng h1) /\ (rng (g2 | m)) in rng (g2 | m) by A113, XBOOLE_0:def 4;
then consider n2 being Element of NAT such that
A118: n2 in dom (g2 | m) and
A119: the Element of (rng h1) /\ (rng (g2 | m)) = (g2 | m) /. n2 by PARTFUN2:2;
A120: (g2 | m) /. n2 in rng (g2 | m) by A118, PARTFUN2:2;
consider i1, i2 being Nat such that
A121: [i1,i2] in Indices G1 and
A122: (g2 | m) /. n2 = G1 * (i1,i2) by A15, A118, GOBOARD1:def 9;
reconsider L = Line (G1,i1) as FinSequence of (TOP-REAL 2) ;
A123: i2 in Seg (width G1) by A96, A121, ZFMISC_1:87;
A124: ( Seg (len L) = dom L & len L = width G1 ) by FINSEQ_1:def 3, MATRIX_0:def 7;
then L /. i2 = L . i2 by A123, PARTFUN1:def 6;
then (g2 | m) /. n2 = L /. i2 by A122, A123, MATRIX_0:def 7;
then (g2 | m) /. n2 in rng L by A123, A124, PARTFUN2:2;
then A125: (rng (g2 | m)) /\ (rng L) <> {} by A120, XBOOLE_0:def 4;
i1 in dom G1 by A96, A121, ZFMISC_1:87;
then A126: mi <= i1 by A39, A125;
the Element of (rng h1) /\ (rng (g2 | m)) = G1 * (n1,k1) by A74, A114, A115;
then i1 = n1 by A119, A121, A122, A117, GOBOARD1:5;
then mi <= mi - 1 by A116, A126, XXREAL_0:2;
hence contradiction by XREAL_1:44; :: thesis:

end;

defpred S₅[ Nat] means ( $1 in dom g1 & ma1 < $1 & g1 /. $1 in rng (Line (G1,ma)) );
A127: mi <= ma by A39, A41;
then A128: mi < ma by A95, XXREAL_0:1;
then ex n being Nat st S₅[n] by A6, A9, A39, A48, A46, GOBOARD1:37;
then A129: ex n being Nat st S₅[n] ;
consider mi1 being Nat such that
A130: ( S₅[mi1] & ( for n being Nat st S₅[n] holds
mi1 <= n ) ) from NAT_1:sch 5(A129);
consider k2 being Element of NAT such that
A131: k2 in dom Lma and
A132: g1 /. mi1 = Lma /. k2 by A130, PARTFUN2:2;
deffunc H₂( Nat) -> Element of the U1 of (TOP-REAL 2) = G1 * ((ma + $1),k2);
consider h2 being FinSequence of (TOP-REAL 2) such that
A133: ( len h2 = l2 & ( for n being Nat st n in dom h2 holds
h2 /. n = H₂(n) ) ) from FINSEQ_4:sch 2();
reconsider Ck2 = Col (G1,k2) as FinSequence of (TOP-REAL 2) ;
dom Lma = Seg (len Lma) by FINSEQ_1:def 3;
then A134: k2 in Seg (width G1) by A131, MATRIX_0:def 7;

A135: now :: thesis:

let n be Nat; :: thesis:
A136: n <= n + ma by NAT_1:11;
assume A137: n in dom h2 ; :: thesis:
then n <= l2 by A133, FINSEQ_3:25;
then A138: ma + n <= ma + l2 by XREAL_1:7;
1 <= n by A137, FINSEQ_3:25;
then 1 <= n + ma by A136, XXREAL_0:2;
hence ma + n in dom G1 by A138, FINSEQ_3:25; :: thesis:

end;

A139: now :: thesis:

let n be Nat; :: thesis:
assume A140: n in dom h2 ; :: thesis:
reconsider m = ma + n, k2 = k2 as Nat ;
take m = m; :: thesis:
take k2 = k2; :: thesis:
ma + n in dom G1 by A135, A140;
hence ( [m,k2] in Indices G1 & h2 /. n = G1 * (m,k2) ) by A134, A133, A96, A140, ZFMISC_1:87; :: thesis:

end;

A141: now :: thesis:

let n be Nat; :: thesis:
assume that
A142: n in dom h2 and
A143: n + 1 in dom h2 ; :: thesis:
ma + (n + 1) in dom G1 by A135, A143;
then A144: [((ma + n) + 1),k2] in Indices G1 by A134, A96, ZFMISC_1:87;
let i1, i2, j1, j2 be Nat; :: thesis:
assume that
A145: [i1,i2] in Indices G1 and
A146: [j1,j2] in Indices G1 and
A147: h2 /. n = G1 * (i1,i2) and
A148: h2 /. (n + 1) = G1 * (j1,j2) ; :: thesis:
h2 /. (n + 1) = G1 * ((ma + (n + 1)),k2) by A133, A143;
then A149: ( j1 = (ma + n) + 1 & j2 = k2 ) by A144, A146, A148, GOBOARD1:5;
ma + n in dom G1 by A135, A142;
then A150: [(ma + n),k2] in Indices G1 by A134, A96, ZFMISC_1:87;
h2 /. n = G1 * ((ma + n),k2) by A133, A142;
then ( i1 = ma + n & i2 = k2 ) by A150, A145, A147, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| = |.(((ma + n) - (ma + n)) + (- 1)).| + 0 by A149, ABSVALUE:2
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

A151: mi1 <= mi1 + 1 by NAT_1:11;
A152: 0 + 1 < width G1 by A3, A92, XREAL_1:6;
A153: len (DelCol (G1,(width G1))) = len G1 by MATRIX_0:def 13;
ma1 <= mi1 by A130;
then reconsider l = (mi1 + 1) - ma1 as Element of NAT by A151, INT_1:5, XXREAL_0:2;
set f1 = g1 | mi1;
defpred S₆[ Nat, Element of (TOP-REAL 2)] means $2 = (g1 | mi1) /. (w + $1);
A154: for n being Nat st n in Seg l holds
ex p being Point of (TOP-REAL 2) st S₆[n,p] ;
consider f being FinSequence of (TOP-REAL 2) such that
A155: ( len f = l & ( for n being Nat st n in Seg l holds
S₆[n,f /. n] ) ) from FINSEQ_4:sch 1(A154);
A156: w + l = mi1 ;
A157: dom f = Seg l by A155, FINSEQ_1:def 3;
set ff = (h1 ^ f) ^ h2;
ma1 + 1 <= mi1 by A130, NAT_1:13;
then ma1 + 1 <= mi1 + 1 by NAT_1:13;
then A158: 1 <= l by XREAL_1:19;

A159: now :: thesis:

suppose A160: mi = 1 ; :: thesis:

1 <= ma1 by A75, A46, FINSEQ_1:1;
then A161: ma1 in Seg mi1 by A130, FINSEQ_1:1;
A162: w + 1 = ma1 ;
A163: 1 in Seg l by A158, FINSEQ_1:1;
h1 = {} by A74, A160;
then (h1 ^ f) ^ h2 = f ^ h2 by FINSEQ_1:34;
then ((h1 ^ f) ^ h2) /. 1 = f /. 1 by A157, A163, FINSEQ_4:68
.= (g1 | mi1) /. ma1 by A155, A163, A162
.= g1 /. ma1 by A130, A161, FINSEQ_4:71 ;
hence ((h1 ^ f) ^ h2) /. 1 in rng (Line (G1,1)) by A46, A160; :: thesis:

end;

suppose A164: mi <> 1 ; :: thesis:

1 <= mi by A39, FINSEQ_3:25;
then 1 < mi by A164, XXREAL_0:1;
then 1 + 1 <= mi by NAT_1:13;
then A165: 1 <= l1 by XREAL_1:19;
then A166: 1 in dom h1 by A74, FINSEQ_3:25;
A167: len (Line (G1,1)) = width G1 by MATRIX_0:def 7;
then A168: k1 in dom L1 by A51, FINSEQ_1:def 3;
dom (Line (G1,1)) = Seg (width G1) by A167, FINSEQ_1:def 3;
then A169: L1 /. k1 = L1 . k1 by A51, PARTFUN1:def 6;
( len (h1 ^ f) = (len h1) + (len f) & 0 <= len f ) by FINSEQ_1:22;
then 0 + 1 <= len (h1 ^ f) by A74, A165, XREAL_1:7;
then 1 in dom (h1 ^ f) by FINSEQ_3:25;
then ((h1 ^ f) ^ h2) /. 1 = (h1 ^ f) /. 1 by FINSEQ_4:68
.= h1 /. 1 by A166, FINSEQ_4:68
.= G1 * (1,k1) by A74, A166
.= L1 /. k1 by A51, A169, MATRIX_0:def 7 ;
hence ((h1 ^ f) ^ h2) /. 1 in rng (Line (G1,1)) by A168, PARTFUN2:2; :: thesis:

end;

A170: for n being Nat st n in Seg l holds
( (g1 | mi1) /. (w + n) = g1 /. (w + n) & w + n in dom g1 )

0 + 1 <= ma1 by A46, FINSEQ_3:25;
then A171: 0 <= ma1 - 1 by XREAL_1:19;
let n be Nat; :: thesis:
assume A172: n in Seg l ; :: thesis:
n <= l by A172, FINSEQ_1:1;
then n + ma1 <= l + ma1 by XREAL_1:7;
then A173: (n + ma1) - 1 <= mi1 by XREAL_1:20;
1 <= n by A172, FINSEQ_1:1;
then 0 + 1 <= (ma1 - 1) + n by A171, XREAL_1:7;
then w + n in Seg mi1 by A173, FINSEQ_1:1;
hence ( (g1 | mi1) /. (w + n) = g1 /. (w + n) & w + n in dom g1 ) by A130, FINSEQ_4:71; :: thesis:

end;

A174: now :: thesis:

let n be Nat; :: thesis:
assume A175: n in dom f ; :: thesis:
then w + n in dom g1 by A170, A157;
then consider i, j being Nat such that
A176: ( [i,j] in Indices G1 & g1 /. (w + n) = G1 * (i,j) ) by A6, GOBOARD1:def 9;
take i = i; :: thesis:
take j = j; :: thesis:
f /. n = (g1 | mi1) /. (w + n) by A155, A157, A175;
hence ( [i,j] in Indices G1 & f /. n = G1 * (i,j) ) by A170, A157, A175, A176; :: thesis:

end;

A177: Seg (len f) = dom f by FINSEQ_1:def 3;
A178: rng f c= rng g1

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider n being Element of NAT such that
A179: n in dom f and
A180: x = f /. n by PARTFUN2:2;
f /. n = (g1 | mi1) /. (w + n) by A155, A177, A179;
then A181: f /. n = g1 /. (w + n) by A170, A155, A177, A179;
w + n in dom g1 by A170, A155, A177, A179;
hence x in rng g1 by A180, A181, PARTFUN2:2; :: thesis:

end;

A182: dom h2 = Seg (len h2) by FINSEQ_1:def 3;

A183: now :: thesis:

suppose A184: ma = len G1 ; :: thesis:

1 <= mi1 by A130, FINSEQ_3:25;
then A185: mi1 in Seg mi1 by FINSEQ_1:1;
A186: len f in dom f by A155, A177, A158, FINSEQ_1:1;
h2 = {} by A133, A184;
then A187: (h1 ^ f) ^ h2 = h1 ^ f by FINSEQ_1:34;
then ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) = ((h1 ^ f) ^ h2) /. ((len h1) + (len f)) by FINSEQ_1:22
.= f /. l by A155, A187, A186, FINSEQ_4:69
.= (g1 | mi1) /. mi1 by A155, A157, A156, A186
.= g1 /. mi1 by A130, A185, FINSEQ_4:71 ;
hence ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line (G1,(len G1))) by A130, A184; :: thesis:

end;

suppose A188: ma <> len G1 ; :: thesis:

ma <= len G1 by A41, FINSEQ_3:25;
then ma < len G1 by A188, XXREAL_0:1;
then ma + 1 <= len G1 by NAT_1:13;
then A189: 1 <= l2 by XREAL_1:19;
then A190: l2 in Seg l2 by FINSEQ_1:1;
A191: len h2 in dom h2 by A133, A189, FINSEQ_3:25;
A192: len (Line (G1,(len G1))) = width G1 by MATRIX_0:def 7;
then A193: k2 in dom Ll by A134, FINSEQ_1:def 3;
k2 in dom Ll by A134, A192, FINSEQ_1:def 3;
then A194: Ll /. k2 = Ll . k2 by PARTFUN1:def 6;
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) = ((h1 ^ f) ^ h2) /. ((len (h1 ^ f)) + (len h2)) by FINSEQ_1:22
.= h2 /. l2 by A133, A191, FINSEQ_4:69
.= G1 * ((ma + l2),k2) by A133, A182, A190
.= Ll /. k2 by A134, A194, MATRIX_0:def 7 ;
hence ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line (G1,(len G1))) by A193, PARTFUN2:2; :: thesis:

end;

A195: 0 + 1 <= (len f) + ((len h1) + (len h2)) by A155, A158, XREAL_1:7;
A196: rng ((h1 ^ f) ^ h2) = (rng (h1 ^ f)) \/ (rng h2) by FINSEQ_1:31
.= ((rng h1) \/ (rng f)) \/ (rng h2) by FINSEQ_1:31 ;
A197: for k being Nat st k in Seg (width G1) & (rng f) /\ (rng (Col (G1,k))) = {} holds
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = {}

A198: len (Col (G1,k2)) = len G1 by MATRIX_0:def 8;
A199: len (Col (G1,k1)) = len G1 by MATRIX_0:def 8;
A200: w + 1 = ma1 ;
let k be Nat; :: thesis:
assume that
A201: k in Seg (width G1) and
A202: (rng f) /\ (rng (Col (G1,k))) = {} ; :: thesis:
set gg = Col (G1,k);
assume A203: (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) <> {} ; :: thesis:
set x = the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k)));
rng ((h1 ^ f) ^ h2) = (rng f) \/ ((rng h1) \/ (rng h2)) by A196, XBOOLE_1:4;
then A204: (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = {} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col (G1,k)))) by A202, XBOOLE_1:23
.= ((rng h1) /\ (rng (Col (G1,k)))) \/ ((rng h2) /\ (rng (Col (G1,k)))) by XBOOLE_1:23 ;

per cases by A203, A204, XBOOLE_0:def 3;

suppose A205: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k))) ; :: thesis:

then the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in rng h1 by XBOOLE_0:def 4;
then consider i being Element of NAT such that
A206: i in dom h1 and
A207: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = h1 /. i by PARTFUN2:2;
A208: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = G1 * (i,k1) by A74, A206, A207;
reconsider y = the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) as Point of (TOP-REAL 2) by A207;
A209: Lmi /. k1 = Lmi . k1 by A49, PARTFUN1:def 6;
A210: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k)) by A205, XBOOLE_0:def 4;
A211: dom (Col (G1,k1)) = Seg (len G1) by A199, FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3 ;
then A212: Ck1 /. mi = Ck1 . mi by A39, PARTFUN1:def 6;
A213: i in dom Ck1 by A97, A206, A211;
Ck1 /. i = Ck1 . i by A97, A206, A211, PARTFUN1:def 6;
then y = Ck1 /. i by A208, A211, A213, MATRIX_0:def 8;
then y in rng Ck1 by A213, PARTFUN2:2;
then A214: k1 = k by A51, A201, A210, GOBOARD1:4;
A215: 1 in Seg l by A158, FINSEQ_1:1;
then ( f /. 1 = (g1 | mi1) /. ma1 & (g1 | mi1) /. ma1 = g1 /. (w + 1) ) by A170, A155, A200;
then f /. 1 = Ck1 /. mi by A39, A50, A51, A209, A212, MATRIX_0:42;
then A216: f /. 1 in rng (Col (G1,k)) by A39, A211, A214, PARTFUN2:2;
f /. 1 in rng f by A157, A215, PARTFUN2:2;
hence contradiction by A202, A216, XBOOLE_0:def 4; :: thesis:

end;

suppose A217: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k))) ; :: thesis:

then the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in rng h2 by XBOOLE_0:def 4;
then consider i being Element of NAT such that
A218: i in dom h2 and
A219: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = h2 /. i by PARTFUN2:2;
A220: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) = G1 * ((ma + i),k2) by A133, A218, A219;
reconsider y = the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) as Point of (TOP-REAL 2) by A219;
A221: Lma /. k2 = Lma . k2 by A131, PARTFUN1:def 6;
A222: the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k)) by A217, XBOOLE_0:def 4;
A223: dom (Col (G1,k2)) = Seg (len G1) by A198, FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3 ;
then A224: Ck2 /. ma = Ck2 . ma by A41, PARTFUN1:def 6;
A225: ma + i in dom Ck2 by A135, A218, A223;
Ck2 /. (ma + i) = Ck2 . (ma + i) by A135, A218, A223, PARTFUN1:def 6;
then y = Ck2 /. (ma + i) by A220, A223, A225, MATRIX_0:def 8;
then y in rng Ck2 by A225, PARTFUN2:2;
then A226: k2 = k by A134, A201, A222, GOBOARD1:4;
A227: l in Seg l by A158, FINSEQ_1:1;
then ( f /. l = (g1 | mi1) /. (w + l) & (g1 | mi1) /. (w + l) = g1 /. (w + l) ) by A170, A155;
then f /. l = Ck2 /. ma by A41, A132, A134, A221, A224, MATRIX_0:42;
then A228: f /. l in rng (Col (G1,k)) by A41, A223, A226, PARTFUN2:2;
f /. l in rng f by A157, A227, PARTFUN2:2;
hence contradiction by A202, A228, XBOOLE_0:def 4; :: thesis:

end;

end;

(rng h2) /\ (rng (g2 | m)) = {}

set x = the Element of (rng h2) /\ (rng (g2 | m));
assume A229: not (rng h2) /\ (rng (g2 | m)) = {} ; :: thesis:
then the Element of (rng h2) /\ (rng (g2 | m)) in rng h2 by XBOOLE_0:def 4;
then consider n1 being Element of NAT such that
A230: n1 in dom h2 and
A231: the Element of (rng h2) /\ (rng (g2 | m)) = h2 /. n1 by PARTFUN2:2;
A232: 1 <= n1 by A230, FINSEQ_3:25;
ma + n1 in dom G1 by A135, A230;
then A233: [(ma + n1),k2] in Indices G1 by A134, A96, ZFMISC_1:87;
the Element of (rng h2) /\ (rng (g2 | m)) in rng (g2 | m) by A229, XBOOLE_0:def 4;
then consider n2 being Element of NAT such that
A234: n2 in dom (g2 | m) and
A235: the Element of (rng h2) /\ (rng (g2 | m)) = (g2 | m) /. n2 by PARTFUN2:2;
consider i1, i2 being Nat such that
A236: [i1,i2] in Indices G1 and
A237: (g2 | m) /. n2 = G1 * (i1,i2) by A15, A234, GOBOARD1:def 9;
reconsider L = Line (G1,i1) as FinSequence of (TOP-REAL 2) ;
A238: i2 in Seg (width G1) by A96, A236, ZFMISC_1:87;
A239: ( Seg (len L) = dom L & len L = width G1 ) by FINSEQ_1:def 3, MATRIX_0:def 7;
then L /. i2 = L . i2 by A238, PARTFUN1:def 6;
then (g2 | m) /. n2 = L /. i2 by A237, A238, MATRIX_0:def 7;
then A240: (g2 | m) /. n2 in rng L by A238, A239, PARTFUN2:2;
(g2 | m) /. n2 in rng (g2 | m) by A234, PARTFUN2:2;
then A241: (rng (g2 | m)) /\ (rng L) <> {} by A240, XBOOLE_0:def 4;
A242: i1 in dom G1 by A96, A236, ZFMISC_1:87;
the Element of (rng h2) /\ (rng (g2 | m)) = G1 * ((ma + n1),k2) by A133, A230, A231;
then i1 = ma + n1 by A235, A236, A237, A233, GOBOARD1:5;
then n1 <= 0 by A41, A242, A241, XREAL_1:29;
hence contradiction by A232; :: thesis:

end;

then (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) = (((rng h1) \/ (rng f)) /\ (rng (g2 | m))) \/ {} by A196, XBOOLE_1:23
.= {} \/ ((rng f) /\ (rng (g2 | m))) by A112, XBOOLE_1:23
.= (rng f) /\ (rng (g2 | m)) ;
then A243: (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) c= (rng g1) /\ (rng g2) by A18, A178, XBOOLE_1:27;
A244: len (DelCol (G1,1)) = len G1 by MATRIX_0:def 13;
then A245: dom (DelCol (G1,1)) = Seg (len G1) by FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3 ;

A246: now :: thesis:

let n be Nat; :: thesis:
assume that
A247: n in dom f and
A248: n + 1 in dom f ; :: thesis:
f /. n = (g1 | mi1) /. (w + n) by A155, A157, A247;
then A249: f /. n = g1 /. (w + n) by A170, A157, A247;
f /. (n + 1) = (g1 | mi1) /. (w + (n + 1)) by A155, A157, A248;
then A250: ( (w + n) + 1 in dom g1 & f /. (n + 1) = g1 /. ((w + n) + 1) ) by A170, A157, A248;
let i1, i2, j1, j2 be Nat; :: thesis:
assume A251: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & f /. n = G1 * (i1,i2) & f /. (n + 1) = G1 * (j1,j2) ) ; :: thesis:
w + n in dom g1 by A170, A157, A247;
hence |.(i1 - j1).| + |.(i2 - j2).| = 1 by A6, A249, A250, A251, GOBOARD1:def 9; :: thesis:

end;

set hf = h1 ^ f;
A252: len ((h1 ^ f) ^ h2) = (len (h1 ^ f)) + (len h2) by FINSEQ_1:22
.= ((len h1) + (len f)) + (len h2) by FINSEQ_1:22 ;

A253: now :: thesis:

let i1, i2, j1, j2 be Nat; :: thesis:
assume that
A254: [i1,i2] in Indices G1 and
A255: [j1,j2] in Indices G1 and
A256: (h1 ^ f) /. (len (h1 ^ f)) = G1 * (i1,i2) and
A257: h2 /. 1 = G1 * (j1,j2) and
len (h1 ^ f) in dom (h1 ^ f) and
A258: 1 in dom h2 ; :: thesis:
ma + 1 in dom G1 by A135, A258;
then A259: [(ma + 1),k2] in Indices G1 by A134, A96, ZFMISC_1:87;
A260: [ma,k2] in Indices G1 by A41, A134, A96, ZFMISC_1:87;
A261: Lma /. k2 = Lma . k2 by A131, PARTFUN1:def 6;
A262: len f in dom f by A155, A157, A158, FINSEQ_1:1;
(h1 ^ f) /. (len (h1 ^ f)) = (h1 ^ f) /. ((len h1) + (len f)) by FINSEQ_1:22
.= f /. (len f) by A262, FINSEQ_4:69
.= (g1 | mi1) /. (w + l) by A155, A157, A262
.= g1 /. mi1 by A170, A155, A157, A262
.= G1 * (ma,k2) by A132, A134, A261, MATRIX_0:def 7 ;
then A263: ( i1 = ma & i2 = k2 ) by A254, A256, A260, GOBOARD1:5;
h2 /. 1 = G1 * ((ma + 1),k2) by A133, A258;
then ( j1 = ma + 1 & j2 = k2 ) by A255, A257, A259, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| = |.(ma - (ma + 1)).| + 0 by A263, ABSVALUE:2
.= |.(- ((ma + 1) - ma)).|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

A264: [mi,k1] in Indices G1 by A39, A51, A96, ZFMISC_1:87;
A265: Lmi /. k1 = Lmi . k1 by A49, PARTFUN1:def 6;
let i1, i2, j1, j2 be Nat; :: thesis:
assume that
A266: [i1,i2] in Indices G1 and
A267: [j1,j2] in Indices G1 and
A268: h1 /. (len h1) = G1 * (i1,i2) and
A269: f /. 1 = G1 * (j1,j2) and
A270: len h1 in dom h1 and
A271: 1 in dom f ; :: thesis:
l1 in dom G1 by A74, A97, A270;
then A272: [l1,k1] in Indices G1 by A51, A96, ZFMISC_1:87;
A273: w + 1 = ma1 ;
then f /. 1 = (g1 | mi1) /. ma1 by A155, A157, A271;
then f /. 1 = g1 /. ma1 by A170, A157, A271, A273
.= G1 * (mi,k1) by A50, A51, A265, MATRIX_0:def 7 ;
then A274: ( j1 = mi & j2 = k1 ) by A267, A269, A264, GOBOARD1:5;
h1 /. (len h1) = G1 * (l1,k1) by A74, A270;
then ( i1 = l1 & i2 = k1 ) by A266, A268, A272, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| = |.((mi - 1) - mi).| + 0 by A274, ABSVALUE:2
.= |.(- 1).|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

then for n being Nat st n in dom (h1 ^ f) & n + 1 in dom (h1 ^ f) holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ f) /. n = G1 * (i1,i2) & (h1 ^ f) /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 by A102, A246, GOBOARD1:24;
then A275: for n being Nat st n in dom ((h1 ^ f) ^ h2) & n + 1 in dom ((h1 ^ f) ^ h2) holds
for m, k, i, j being Nat st [m,k] in Indices G1 & [i,j] in Indices G1 & ((h1 ^ f) ^ h2) /. n = G1 * (m,k) & ((h1 ^ f) ^ h2) /. (n + 1) = G1 * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 by A141, A253, GOBOARD1:24;

let n be Nat; :: thesis:
assume A276: n in dom h1 ; :: thesis:
reconsider k1 = k1 as Nat ;
take i = n; :: thesis:
take k1 = k1; :: thesis:
n in dom G1 by A97, A276;
hence ( [i,k1] in Indices G1 & h1 /. n = G1 * (i,k1) ) by A74, A51, A96, A276, ZFMISC_1:87; :: thesis:

end;

then for n being Nat st n in dom (h1 ^ f) holds
ex i, j being Nat st
( [i,j] in Indices G1 & (h1 ^ f) /. n = G1 * (i,j) ) by A174, GOBOARD1:23;
then for n being Nat st n in dom ((h1 ^ f) ^ h2) holds
ex i, j being Nat st
( [i,j] in Indices G1 & ((h1 ^ f) ^ h2) /. n = G1 * (i,j) ) by A139, GOBOARD1:23;
then A277: (h1 ^ f) ^ h2 is_sequence_on G1 by A275, GOBOARD1:def 9;
A278: Seg (len ((h1 ^ f) ^ h2)) = dom ((h1 ^ f) ^ h2) by FINSEQ_1:def 3;
then A279: len ((h1 ^ f) ^ h2) in dom ((h1 ^ f) ^ h2) by A252, A195, FINSEQ_1:1;
A280: 1 in dom ((h1 ^ f) ^ h2) by A252, A195, A278, FINSEQ_1:1;
thus (rng g1) /\ (rng g2) <> {} :: thesis:

per cases ) /\ (rng (Col (G1,1))) = {} or (rng f) /\ (rng (Col (G1,1))) <> {} ) ;

suppose A281: (rng f) /\ (rng (Col (G1,1))) = {} ; :: thesis:

set D = DelCol (G1,1);
A282: 1 in Seg (width G1) by A152, FINSEQ_1:1;
A283: DelCol (G1,1) is empty-yielding by A152, A282, MATRIX_0:65;
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,1))) = {} by A31, A197, A281;
then A284: rng ((h1 ^ f) ^ h2) misses rng (Col (G1,1)) by XBOOLE_0:def 7;
then A285: ( (h1 ^ f) ^ h2 is_sequence_on DelCol (G1,1) & ((h1 ^ f) ^ h2) /. 1 in rng (Line ((DelCol (G1,1)),1)) ) by A31, A26, A277, A159, A152, A280, GOBOARD1:25, MATRIX_0:75;
A286: ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line ((DelCol (G1,1)),(len (DelCol (G1,1))))) by A31, A27, A183, A152, A244, A279, A284, MATRIX_0:75;
defpred S₇[ Nat] means ( $1 in dom (g2 | m) & (g2 | m) /. $1 in rng (Col (G1,1)) );
A287: ex m being Nat st S₇[m]

take 1 ; :: thesis:
thus S₇[1] by A10, A13, A32, FINSEQ_3:25, FINSEQ_4:92; :: thesis:

end;

A288: for m being Nat st S₇[m] holds
m <= len (g2 | m) by FINSEQ_3:25;
consider m being Nat such that
A289: ( S₇[m] & ( for k being Nat st S₇[k] holds
k <= m ) ) from NAT_1:sch 6(A288, A287);
reconsider m = m as Nat ;
reconsider p = (g2 | m) /. m as Point of (TOP-REAL 2) ;

A290: now :: thesis:

assume A291: m >= len (g2 | m) ; :: thesis:
m <= len (g2 | m) by A289, FINSEQ_3:25;
then p in rng (Col (G1,(width G1))) by A28, A291, XXREAL_0:1;
then 1 = k + 1 by A3, A31, A73, A289, GOBOARD1:4;
hence contradiction by A91; :: thesis:

end;

then reconsider ll = (len (g2 | m)) - m as Element of NAT by INT_1:5;
deffunc H₃( Nat) -> Element of the U1 of (TOP-REAL 2) = (g2 | m) /. (m + $1);
consider t being FinSequence of (TOP-REAL 2) such that
A292: ( len t = ll & ( for n being Nat st n in dom t holds
t /. n = H₃(n) ) ) from FINSEQ_4:sch 2();
A293: dom t = Seg ll by A292, FINSEQ_1:def 3;
A294: rng t c= rng (g2 | m)

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng t ; :: thesis:
then consider x being Element of NAT such that
A295: x in dom t and
A296: t /. x = y by PARTFUN2:2;
x <= ll by A293, A295, FINSEQ_1:1;
then A297: m + x <= m + ll by XREAL_1:7;
A298: x <= x + m by NAT_1:11;
1 <= x by A293, A295, FINSEQ_1:1;
then 1 <= x + m by A298, XXREAL_0:2;
then m + x in dom (g2 | m) by A297, FINSEQ_3:25;
then (g2 | m) /. (m + x) in rng (g2 | m) by PARTFUN2:2;
hence y in rng (g2 | m) by A292, A295, A296; :: thesis:

end;

A299: for n being Nat st n in dom t holds
m + n in dom (g2 | m)

let n be Nat; :: thesis:
A300: n <= n + m by NAT_1:11;
assume A301: n in dom t ; :: thesis:
then n <= ll by A293, FINSEQ_1:1;
then A302: m + n <= m + ll by XREAL_1:7;
1 <= n by A293, A301, FINSEQ_1:1;
then 1 <= n + m by A300, XXREAL_0:2;
hence m + n in dom (g2 | m) by A302, FINSEQ_3:25; :: thesis:

end;

A303: Seg (len t) = dom t by FINSEQ_1:def 3;
reconsider t = t as FinSequence of (TOP-REAL 2) ;
A304: width (DelCol (G1,1)) = k by A3, A31, MATRIX_0:63;
A305: Indices (DelCol (G1,1)) = [:(dom (DelCol (G1,1))),(Seg (width (DelCol (G1,1)))):] by MATRIX_0:def 4;

A306: now :: thesis:

let n be Nat; :: thesis:
assume A307: n in dom t ; :: thesis:
then m + n in dom (g2 | m) by A299;
then consider i1, i2 being Nat such that
A308: [i1,i2] in Indices G1 and
A309: (g2 | m) /. (m + n) = G1 * (i1,i2) by A15, GOBOARD1:def 9;
A310: i2 in Seg (width G1) by A96, A308, ZFMISC_1:87;
then A311: 1 <= i2 by FINSEQ_1:1;
then reconsider l = i2 - 1 as Element of NAT by INT_1:5;
reconsider Ci2 = Col (G1,i2) as FinSequence of (TOP-REAL 2) ;
A312: i1 in dom G1 by A96, A308, ZFMISC_1:87;
len Ci2 = len G1 by MATRIX_0:def 8;
then A313: dom Ci2 = Seg (len G1) by FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3 ;
then Ci2 /. i1 = Ci2 . i1 by A312, PARTFUN1:def 6;
then Ci2 /. i1 = G1 * (i1,i2) by A312, MATRIX_0:def 8;
then A314: (g2 | m) /. (m + n) in rng (Col (G1,i2)) by A309, A312, A313, PARTFUN2:2;

1 <= n by A293, A307, FINSEQ_1:1;
then A315: m + 1 <= m + n by XREAL_1:7;
assume i2 = 1 ; :: thesis:
then m + n <= m by A289, A299, A307, A314;
then m + 1 <= m by A315, XXREAL_0:2;
then 1 <= m - m by XREAL_1:19;
then 1 <= 0 ;
hence contradiction ; :: thesis:

end;

then 1 < i2 by A311, XXREAL_0:1;
then 1 + 1 <= i2 by NAT_1:13;
then A316: 1 <= l by XREAL_1:19;
reconsider i1 = i1, l = l as Nat ;
take i1 = i1; :: thesis:
take l = l; :: thesis:
A317: t /. n = (g2 | m) /. (m + n) by A292, A307;
i2 <= width G1 by A310, FINSEQ_1:1;
then A318: l <= width (DelCol (G1,1)) by A3, A304, XREAL_1:20;
then l in Seg (width (DelCol (G1,1))) by A316, FINSEQ_1:1;
hence [i1,l] in Indices (DelCol (G1,1)) by A245, A305, A312, ZFMISC_1:87; :: thesis:
l + 1 = i2 ;
hence t /. n = (DelCol (G1,1)) * (i1,l) by A3, A31, A304, A309, A312, A317, A316, A318, MATRIX_0:70; :: thesis:

end;

0 < width (DelCol (G1,1)) by A283, MATRIX_0:def 10, NAT_1:3;
then A319: 0 + 1 <= width (DelCol (G1,1)) by NAT_1:13;
then A320: ( Col ((DelCol (G1,1)),1) = Col (G1,(1 + 1)) & 1 + 1 in Seg (width G1) ) by A3, A31, A304, MATRIX_0:68;
m + 1 <= len (g2 | m) by A290, NAT_1:13;
then A321: 1 <= len t by A292, XREAL_1:19;
then t /. 1 = (g2 | m) /. (m + 1) by A292, A303, FINSEQ_1:1;
then A322: t /. 1 in rng (Col ((DelCol (G1,1)),1)) by A32, A15, A28, A31, A289, A320, GOBOARD1:32;

let n be Nat; :: thesis:
assume that
A323: n in dom t and
A324: n + 1 in dom t ; :: thesis:
let i1, i2, j1, j2 be Nat; :: thesis:
assume that
A325: [i1,i2] in Indices (DelCol (G1,1)) and
A326: [j1,j2] in Indices (DelCol (G1,1)) and
A327: t /. n = (DelCol (G1,1)) * (i1,i2) and
A328: t /. (n + 1) = (DelCol (G1,1)) * (j1,j2) ; :: thesis:
A329: i1 in dom (DelCol (G1,1)) by A305, A325, ZFMISC_1:87;
i2 in Seg k by A304, A305, A325, ZFMISC_1:87;
then A330: ( 1 <= i2 & i2 <= k ) by FINSEQ_1:1;
then i2 + 1 in Seg (width G1) by A3, A31, A245, A329, MATRIX_0:70;
then A331: [i1,(i2 + 1)] in Indices G1 by A96, A245, A329, ZFMISC_1:87;
t /. n = (g2 | m) /. (m + n) by A292, A323;
then A332: (g2 | m) /. (m + n) = G1 * (i1,(i2 + 1)) by A3, A31, A245, A327, A329, A330, MATRIX_0:70;
m + (n + 1) = (m + n) + 1 ;
then A333: (m + n) + 1 in dom (g2 | m) by A299, A324;
A334: j1 in dom (DelCol (G1,1)) by A305, A326, ZFMISC_1:87;
j2 in Seg k by A304, A305, A326, ZFMISC_1:87;
then A335: ( 1 <= j2 & j2 <= k ) by FINSEQ_1:1;
then j2 + 1 in Seg (width G1) by A3, A31, A245, A329, MATRIX_0:70;
then A336: [j1,(j2 + 1)] in Indices G1 by A96, A245, A334, ZFMISC_1:87;
t /. (n + 1) = (g2 | m) /. (m + (n + 1)) by A292, A324;
then A337: (g2 | m) /. ((m + n) + 1) = G1 * (j1,(j2 + 1)) by A3, A31, A245, A328, A334, A335, MATRIX_0:70;
m + n in dom (g2 | m) by A299, A323;
hence 1 = |.(i1 - j1).| + |.((i2 + 1) - (j2 + 1)).| by A15, A332, A337, A331, A336, A333, GOBOARD1:def 9
.= |.(i1 - j1).| + |.(i2 - j2).| ;
:: thesis:

end;

then A338: t is_sequence_on DelCol (G1,1) by A306, GOBOARD1:def 9;
set x = the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng t);
A339: (rng ((h1 ^ f) ^ h2)) /\ (rng t) c= (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) by A294, XBOOLE_1:26;
len t in Seg ll by A292, A321, FINSEQ_1:1;
then t /. (len t) = (g2 | m) /. (m + ll) by A292, A303
.= (g2 | m) /. (len (g2 | m)) ;
then t /. (len t) in rng (Col ((DelCol (G1,1)),(width (DelCol (G1,1))))) by A3, A28, A31, A304, A319, MATRIX_0:68;
then (rng ((h1 ^ f) ^ h2)) /\ (rng t) <> {} by A2, A92, A252, A195, A304, A321, A322, A338, A285, A286, A283;
then the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng t) in (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) by A339;
hence (rng g1) /\ (rng g2) <> {} by A243; :: thesis:

end;

suppose A340: (rng f) /\ (rng (Col (G1,1))) <> {} ; :: thesis:

set D = DelCol (G1,(width G1));
A341: DelCol (G1,(width G1)) is empty-yielding by A93, A94, MATRIX_0:65;
A342: 0 + 1 < k + 1 by A92, XREAL_1:6;

per cases ) /\ (rng (Col (G1,(width G1)))) = {} or (rng f) /\ (rng (Col (G1,(width G1)))) <> {} ) ;

suppose (rng f) /\ (rng (Col (G1,(width G1)))) = {} ; :: thesis:

then (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (G1,(width G1)))) = {} by A73, A197;
then A343: rng ((h1 ^ f) ^ h2) misses rng (Col (G1,(width G1))) by XBOOLE_0:def 7;
then A344: (h1 ^ f) ^ h2 is_sequence_on DelCol (G1,(width G1)) by A73, A277, A152, GOBOARD1:25;
consider t being FinSequence of (TOP-REAL 2) such that
A345: ( t /. 1 in rng (Col ((DelCol (G1,(width G1))),1)) & t /. (len t) in rng (Col ((DelCol (G1,(width G1))),(width (DelCol (G1,(width G1)))))) & 1 <= len t & t is_sequence_on DelCol (G1,(width G1)) ) and
A346: rng t c= rng (g2 | m) by A3, A32, A15, A14, A28, A342, GOBOARD1:35;
set x = the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng t);
A347: (rng ((h1 ^ f) ^ h2)) /\ (rng t) c= (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) by A346, XBOOLE_1:26;
A348: width (DelCol (G1,(width G1))) = k by A3, A73, MATRIX_0:63;
( ((h1 ^ f) ^ h2) /. 1 in rng (Line ((DelCol (G1,(width G1))),1)) & ((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) in rng (Line ((DelCol (G1,(width G1))),(len (DelCol (G1,(width G1)))))) ) by A73, A26, A27, A159, A183, A152, A153, A280, A279, A343, MATRIX_0:75;
then (rng ((h1 ^ f) ^ h2)) /\ (rng t) <> {} by A2, A92, A252, A195, A345, A348, A344, A341;
then the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng t) in (rng ((h1 ^ f) ^ h2)) /\ (rng (g2 | m)) by A347;
hence (rng g1) /\ (rng g2) <> {} by A243; :: thesis:

end;

suppose A349: (rng f) /\ (rng (Col (G1,(width G1)))) <> {} ; :: thesis:

A350: f is_sequence_on G1 by A174, A246, GOBOARD1:def 9;
then consider t being FinSequence of (TOP-REAL 2) such that
A351: rng t c= rng f and
A352: ( t /. 1 in rng (Col (G1,1)) & t /. (len t) in rng (Col (G1,(width G1))) & 1 <= len t & t is_sequence_on G1 ) by A340, A349, GOBOARD1:36;
consider tt being FinSequence of (TOP-REAL 2) such that
A353: ( tt /. 1 in rng (Col ((DelCol (G1,(width G1))),1)) & tt /. (len tt) in rng (Col ((DelCol (G1,(width G1))),(width (DelCol (G1,(width G1)))))) & 1 <= len tt & tt is_sequence_on DelCol (G1,(width G1)) ) and
A354: rng tt c= rng t by A3, A342, A352, GOBOARD1:35;
A355: ( Seg (len Lma) = dom Lma & len Lma = width G1 ) by FINSEQ_1:def 3, MATRIX_0:def 7;
reconsider lg = (len (g2 | m)) - 1 as Element of NAT by A32, INT_1:5;
defpred S₇[ Nat] means ( $1 in dom (g2 | m) & (g2 | m) /. $1 in rng (Line (G1,mi)) );
defpred S₈[ Nat] means ( $1 in dom (g2 | m) & (g2 | m) /. $1 in rng (Line (G1,ma)) );
A356: lg <= len (g2 | m) by XREAL_1:43;

A357: now :: thesis:

set x = the Element of (rng (g2 | m)) /\ (rng (Line (G1,mi)));
the Element of (rng (g2 | m)) /\ (rng (Line (G1,mi))) in rng (g2 | m) by A39, XBOOLE_0:def 4;
then consider n being Element of NAT such that
A358: ( n in dom (g2 | m) & the Element of (rng (g2 | m)) /\ (rng (Line (G1,mi))) = (g2 | m) /. n ) by PARTFUN2:2;
reconsider n = n as Nat ;
take n = n; :: thesis:
thus S₇[n] by A39, A358, XBOOLE_0:def 4; :: thesis:

end;

consider pf being Nat such that
A359: ( S₇[pf] & ( for n being Nat st S₇[n] holds
pf <= n ) ) from NAT_1:sch 5(A357);
defpred S₉[ Nat] means ( $1 in dom f implies for m being Nat st m in dom G1 & f /. $1 in rng (Line (G1,m)) holds
mi <= m );
reconsider C = Col (G1,(width G1)), Li = Line (G1,mi), La = Line (G1,ma) as FinSequence of (TOP-REAL 2) ;
A360: lg + 1 = len (g2 | m) ;

A361: now :: thesis:

set x = the Element of (rng (g2 | m)) /\ (rng (Line (G1,ma)));
the Element of (rng (g2 | m)) /\ (rng (Line (G1,ma))) in rng (g2 | m) by A41, XBOOLE_0:def 4;
then consider n being Element of NAT such that
A362: ( n in dom (g2 | m) & the Element of (rng (g2 | m)) /\ (rng (Line (G1,ma))) = (g2 | m) /. n ) by PARTFUN2:2;
reconsider n = n as Nat ;
take n = n; :: thesis:
thus S₈[n] by A41, A362, XBOOLE_0:def 4; :: thesis:

end;

consider pl being Nat such that
A363: ( S₈[pl] & ( for n being Nat st S₈[n] holds
pl <= n ) ) from NAT_1:sch 5(A361);
reconsider pf = pf, pl = pl as Nat ;
A364: 1 <= pf by A359, FINSEQ_3:25;
consider K2 being Element of NAT such that
A365: K2 in dom Lma and
A366: (g2 | m) /. pl = Lma /. K2 by A363, PARTFUN2:2;
reconsider CK2 = Col (G1,K2) as FinSequence of (TOP-REAL 2) ;
consider K1 being Element of NAT such that
A367: K1 in dom Li and
A368: (g2 | m) /. pf = Li /. K1 by A359, PARTFUN2:2;
reconsider CK1 = Col (G1,K1) as FinSequence of (TOP-REAL 2) ;
deffunc H₃( Nat) -> Element of the U1 of (TOP-REAL 2) = G1 * ($1,K1);
consider h1 being FinSequence of (TOP-REAL 2) such that
A369: ( len h1 = l1 & ( for n being Nat st n in dom h1 holds
h1 /. n = H₃(n) ) ) from FINSEQ_4:sch 2();
A370: for k being Nat st S₉[k] holds
S₉[k + 1]

let k be Nat; :: thesis:
assume A371: S₉[k] ; :: thesis:
assume A372: k + 1 in dom f ; :: thesis:
let m be Nat; :: thesis:
assume A373: ( m in dom G1 & f /. (k + 1) in rng (Line (G1,m)) ) ; :: thesis:

suppose A374: k = 0 ; :: thesis:

( w + 1 = ma1 & 1 in Seg l ) by A158, FINSEQ_1:1;
then ( f /. 1 = (g1 | mi1) /. ma1 & (g1 | mi1) /. ma1 = g1 /. ma1 ) by A170, A155;
then f /. (k + 1) in rng Li by A49, A50, A374, PARTFUN2:2;
hence mi <= m by A39, A373, GOBOARD1:3; :: thesis:

end;

suppose k <> 0 ; :: thesis:

then 0 < k ;
then A375: 0 + 1 <= k by NAT_1:13;
k + 1 <= len f by A372, FINSEQ_3:25;
then A376: k <= len f by NAT_1:13;
then A377: k in dom f by A375, FINSEQ_3:25;
then consider i1, i2 being Nat such that
A378: [i1,i2] in Indices G1 and
A379: f /. k = G1 * (i1,i2) by A174;
A380: i2 in Seg (width G1) by A96, A378, ZFMISC_1:87;
consider j1, j2 being Nat such that
A381: [j1,j2] in Indices G1 and
A382: f /. (k + 1) = G1 * (j1,j2) by A174, A372;
reconsider Lj1 = Line (G1,j1) as FinSequence of (TOP-REAL 2) ;
A383: j2 in Seg (width G1) by A96, A381, ZFMISC_1:87;
A384: ( Seg (len Lj1) = dom Lj1 & len Lj1 = width G1 ) by FINSEQ_1:def 3, MATRIX_0:def 7;
then Lj1 /. j2 = Lj1 . j2 by A383, PARTFUN1:def 6;
then f /. (k + 1) = Lj1 /. j2 by A382, A383, MATRIX_0:def 7;
then A385: f /. (k + 1) in rng Lj1 by A383, A384, PARTFUN2:2;
A386: j1 in dom G1 by A96, A381, ZFMISC_1:87;
reconsider Li1 = Line (G1,i1) as FinSequence of (TOP-REAL 2) ;
A387: i1 in dom G1 by A96, A378, ZFMISC_1:87;
A388: ( Seg (len Li1) = dom Li1 & len Li1 = width G1 ) by FINSEQ_1:def 3, MATRIX_0:def 7;
then A389: Li1 /. i2 = Li1 . i2 by A380, PARTFUN1:def 6;
then f /. k = Li1 /. i2 by A379, A380, MATRIX_0:def 7;
then A390: f /. k in rng Li1 by A380, A388, PARTFUN2:2;
then A391: mi <= i1 by A371, A375, A376, A387, FINSEQ_3:25;

per cases by A391, XXREAL_0:1;

suppose A392: mi = i1 ; :: thesis:

g1 /. (w + k) = (g1 | mi1) /. (w + k) by A170, A157, A377
.= f /. k by A155, A157, A377
.= Li1 /. i2 by A379, A380, A389, MATRIX_0:def 7 ;
then g1 /. (w + k) in rng (Line (G1,mi)) by A380, A388, A392, PARTFUN2:2;
then A393: w + k <= ma1 by A46, A170, A157, A377;
w + 1 <= w + k by A375, XREAL_1:7;
then w + k = ma1 by A393, XXREAL_0:1;
then A394: ma1 + 1 = w + (k + 1) ;
mi + 1 <= ma by A128, NAT_1:13;
then A395: mi + 1 <= len G1 by A48, XXREAL_0:2;
1 <= mi + 1 by A42, NAT_1:13;
then A396: mi + 1 in dom G1 by A395, FINSEQ_3:25;
( f /. (k + 1) = (g1 | mi1) /. (w + (k + 1)) & (g1 | mi1) /. (w + (k + 1)) = g1 /. (w + (k + 1)) ) by A170, A155, A157, A372;
then f /. (k + 1) in rng (Line (G1,(mi + 1))) by A4, A6, A9, A39, A46, A394, A396, GOBOARD1:28;
then m = mi + 1 by A373, A396, GOBOARD1:3;
hence mi <= m by NAT_1:11; :: thesis:

end;

suppose A397: mi < i1 ; :: thesis:

per cases by A350, A372, A377, A387, A390, GOBOARD1:27;

suppose f /. (k + 1) in rng (Line (G1,i1)) ; :: thesis:

hence mi <= m by A373, A387, A397, GOBOARD1:3; :: thesis:

end;

suppose for l being Nat st f /. (k + 1) in rng (Line (G1,l)) & l in dom G1 holds
|.(i1 - l).| = 1 ; :: thesis:

then A398: |.(i1 - j1).| = 1 by A386, A385;

per cases by A398, SEQM_3:41;

suppose A399: ( j1 < i1 & i1 = j1 + 1 ) ; :: thesis:

then mi <= i1 - 1 by A397, NAT_1:13;
hence mi <= m by A373, A386, A385, A399, GOBOARD1:3; :: thesis:

end;

suppose ( i1 < j1 & j1 = i1 + 1 ) ; :: thesis:

then mi < j1 by A397, XXREAL_0:2;
hence mi <= m by A373, A386, A385, GOBOARD1:3; :: thesis:

end;

hence mi <= m ; :: thesis:

end;

hence mi <= m ; :: thesis:

end;

hence mi <= m ; :: thesis:

end;

hence mi <= m ; :: thesis:

end;

A400: ( Seg (len Li) = dom Li & len Li = width G1 ) by FINSEQ_1:def 3, MATRIX_0:def 7;

A401: now :: thesis:

let n be Nat; :: thesis:
A402: l1 <= mi by XREAL_1:43;
assume A403: n in dom h1 ; :: thesis:
then A404: 1 <= n by FINSEQ_3:25;
n <= l1 by A369, A403, FINSEQ_3:25;
then A405: n <= mi by A402, XXREAL_0:2;
mi <= len G1 by A39, FINSEQ_3:25;
then n <= len G1 by A405, XXREAL_0:2;
hence n in dom G1 by A404, FINSEQ_3:25; :: thesis:

end;

A406: now :: thesis:

let n be Nat; :: thesis:
assume A407: n in dom h1 ; :: thesis:
reconsider i = n, K1 = K1 as Nat ;
take i = i; :: thesis:
take K1 = K1; :: thesis:
n in dom G1 by A401, A407;
hence ( [i,K1] in Indices G1 & h1 /. n = G1 * (i,K1) ) by A96, A367, A400, A369, A407, ZFMISC_1:87; :: thesis:

end;

A408: now :: thesis:

let n be Nat; :: thesis:
assume that
A409: n in dom h1 and
A410: n + 1 in dom h1 ; :: thesis:
n + 1 in dom G1 by A401, A410;
then A411: [(n + 1),K1] in Indices G1 by A96, A367, A400, ZFMISC_1:87;
let i1, i2, j1, j2 be Nat; :: thesis:
assume that
A412: [i1,i2] in Indices G1 and
A413: [j1,j2] in Indices G1 and
A414: h1 /. n = G1 * (i1,i2) and
A415: h1 /. (n + 1) = G1 * (j1,j2) ; :: thesis:
h1 /. (n + 1) = G1 * ((n + 1),K1) by A369, A410;
then A416: ( j1 = n + 1 & j2 = K1 ) by A411, A413, A415, GOBOARD1:5;
n in dom G1 by A401, A409;
then A417: [n,K1] in Indices G1 by A96, A367, A400, ZFMISC_1:87;
h1 /. n = G1 * (n,K1) by A369, A409;
then ( i1 = n & i2 = K1 ) by A417, A412, A414, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| = |.((n - n) + (- 1)).| + 0 by A416, ABSVALUE:2
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

A418: pf <= len (g2 | m) by A359, FINSEQ_3:25;
A419: Lma /. K2 = Lma . K2 by A365, PARTFUN1:def 6;
then A420: (g2 | m) /. pl = G1 * (ma,K2) by A365, A366, A355, MATRIX_0:def 7;
deffunc H₄( Nat) -> Element of the U1 of (TOP-REAL 2) = G1 * ((ma + $1),K2);
consider h2 being FinSequence of (TOP-REAL 2) such that
A421: ( len h2 = l2 & ( for n being Nat st n in dom h2 holds
h2 /. n = H₄(n) ) ) from FINSEQ_4:sch 2();
A422: S₉[ 0 ] by FINSEQ_3:25;
A423: for n being Nat holds S₉[n] from NAT_1:sch 2(A422, A370);
A424: (rng h1) /\ (rng tt) = {}

set x = the Element of (rng h1) /\ (rng tt);
assume A425: not (rng h1) /\ (rng tt) = {} ; :: thesis:
then the Element of (rng h1) /\ (rng tt) in rng h1 by XBOOLE_0:def 4;
then consider i2 being Element of NAT such that
A426: i2 in dom h1 and
A427: h1 /. i2 = the Element of (rng h1) /\ (rng tt) by PARTFUN2:2;
Seg (len h1) = dom h1 by FINSEQ_1:def 3;
then A428: ( l1 < mi & i2 <= l1 ) by A369, A426, FINSEQ_1:1, XREAL_1:44;
i2 in dom G1 by A401, A426;
then A429: [i2,K1] in Indices G1 by A96, A367, A400, ZFMISC_1:87;
the Element of (rng h1) /\ (rng tt) in rng tt by A425, XBOOLE_0:def 4;
then the Element of (rng h1) /\ (rng tt) in rng t by A354;
then consider i1 being Element of NAT such that
A430: i1 in dom f and
A431: f /. i1 = the Element of (rng h1) /\ (rng tt) by A351, PARTFUN2:2;
consider n1, n2 being Nat such that
A432: [n1,n2] in Indices G1 and
A433: f /. i1 = G1 * (n1,n2) by A174, A430;
reconsider Ln1 = Line (G1,n1) as FinSequence of (TOP-REAL 2) ;
A434: n2 in Seg (width G1) by A96, A432, ZFMISC_1:87;
A435: ( Seg (len Ln1) = dom Ln1 & len Ln1 = width G1 ) by FINSEQ_1:def 3, MATRIX_0:def 7;
then Ln1 /. n2 = Ln1 . n2 by A434, PARTFUN1:def 6;
then f /. i1 = Ln1 /. n2 by A433, A434, MATRIX_0:def 7;
then A436: f /. i1 in rng Ln1 by A434, A435, PARTFUN2:2;
n1 in dom G1 by A96, A432, ZFMISC_1:87;
then A437: mi <= n1 by A423, A430, A436;
the Element of (rng h1) /\ (rng tt) = G1 * (i2,K1) by A369, A426, A427;
then i2 = n1 by A431, A432, A433, A429, GOBOARD1:5;
hence contradiction by A437, A428, XXREAL_0:2; :: thesis:

end;

defpred S₁₀[ Nat] means ( $1 in dom f implies for m being Nat st m in dom G1 & f /. $1 in rng (Line (G1,m)) holds
m <= ma );
A438: for k being Nat st S₁₀[k] holds
S₁₀[k + 1]

let k be Nat; :: thesis:
assume A439: S₁₀[k] ; :: thesis:
assume A440: k + 1 in dom f ; :: thesis:
let m be Nat; :: thesis:
assume A441: ( m in dom G1 & f /. (k + 1) in rng (Line (G1,m)) ) ; :: thesis:

suppose A442: k = 0 ; :: thesis:

1 in Seg l by A158, FINSEQ_1:1;
then ( f /. 1 = (g1 | mi1) /. (w + 1) & (g1 | mi1) /. (w + 1) = g1 /. (w + 1) ) by A170, A155;
then f /. (k + 1) in rng Li by A49, A50, A442, PARTFUN2:2;
hence m <= ma by A39, A127, A441, GOBOARD1:3; :: thesis:

end;

suppose A443: k <> 0 ; :: thesis:

A444: k + 1 <= len f by A177, A440, FINSEQ_1:1;
then A445: k <= len f by NAT_1:13;
consider j1, j2 being Nat such that
A446: [j1,j2] in Indices G1 and
A447: f /. (k + 1) = G1 * (j1,j2) by A174, A440;
reconsider Lj1 = Line (G1,j1) as FinSequence of (TOP-REAL 2) ;
A448: j2 in Seg (width G1) by A96, A446, ZFMISC_1:87;
A449: ( Seg (len Lj1) = dom Lj1 & len Lj1 = width G1 ) by FINSEQ_1:def 3, MATRIX_0:def 7;
then Lj1 /. j2 = Lj1 . j2 by A448, PARTFUN1:def 6;
then f /. (k + 1) = Lj1 /. j2 by A447, A448, MATRIX_0:def 7;
then A450: f /. (k + 1) in rng Lj1 by A448, A449, PARTFUN2:2;
A451: j1 in dom G1 by A96, A446, ZFMISC_1:87;
then A452: j1 = m by A441, A450, GOBOARD1:3;
0 < k by A443;
then A453: 0 + 1 <= k by NAT_1:13;
then A454: k in dom f by A445, FINSEQ_3:25;
then consider i1, i2 being Nat such that
A455: [i1,i2] in Indices G1 and
A456: f /. k = G1 * (i1,i2) by A174;
reconsider Li1 = Line (G1,i1) as FinSequence of (TOP-REAL 2) ;
A457: i2 in Seg (width G1) by A96, A455, ZFMISC_1:87;
A458: ( Seg (len Li1) = dom Li1 & len Li1 = width G1 ) by FINSEQ_1:def 3, MATRIX_0:def 7;
then Li1 /. i2 = Li1 . i2 by A457, PARTFUN1:def 6;
then f /. k = Li1 /. i2 by A456, A457, MATRIX_0:def 7;
then A459: f /. k in rng Li1 by A457, A458, PARTFUN2:2;
A460: i1 in dom G1 by A96, A455, ZFMISC_1:87;
then A461: i1 <= ma by A439, A453, A445, A459, FINSEQ_3:25;

per cases by A461, XXREAL_0:1;

case A462: ma = i1 ; :: thesis:

A463: w + 1 <= w + k by A453, XREAL_1:7;
A464: ( f /. k = (g1 | mi1) /. (w + k) & (g1 | mi1) /. (w + k) = g1 /. (w + k) ) by A170, A155, A157, A454;
then ma1 <> w + k by A39, A41, A46, A95, A459, A462, GOBOARD1:3;
then ma1 < w + k by A463, XXREAL_0:1;
then A465: mi1 <= w + k by A130, A170, A157, A454, A459, A462, A464;
w + k <= mi1 by A155, A156, A445, XREAL_1:7;
then w + k = mi1 by A465, XXREAL_0:1;
hence contradiction by A155, A444, NAT_1:13; :: thesis:

end;

case A466: i1 < ma ; :: thesis:

per cases by A350, A440, A454, A460, A459, GOBOARD1:27;

suppose f /. (k + 1) in rng (Line (G1,i1)) ; :: thesis:

hence m <= ma by A441, A460, A466, GOBOARD1:3; :: thesis:

end;

suppose for l being Nat st f /. (k + 1) in rng (Line (G1,l)) & l in dom G1 holds
|.(i1 - l).| = 1 ; :: thesis:

then A467: |.(i1 - j1).| = 1 by A451, A450;

per cases by A467, SEQM_3:41;

suppose ( j1 < i1 & i1 = j1 + 1 ) ; :: thesis:

hence m <= ma by A452, A466, XXREAL_0:2; :: thesis:

end;

suppose ( i1 < j1 & j1 = i1 + 1 ) ; :: thesis:

hence m <= ma by A452, A466, NAT_1:13; :: thesis:

end;

hence m <= ma ; :: thesis:

end;

hence m <= ma ; :: thesis:

end;

hence m <= ma ; :: thesis:

end;

hence m <= ma ; :: thesis:

end;

A468: Seg (len h1) = dom h1 by FINSEQ_1:def 3;

A469: now :: thesis:

let n be Nat; :: thesis:
A470: n <= n + ma by NAT_1:11;
assume A471: n in dom h2 ; :: thesis:
then n <= l2 by A421, FINSEQ_3:25;
then A472: ma + n <= ma + l2 by XREAL_1:7;
1 <= n by A471, FINSEQ_3:25;
then 1 <= n + ma by A470, XXREAL_0:2;
hence ma + n in dom G1 by A472, FINSEQ_3:25; :: thesis:

end;

A473: now :: thesis:

let n be Nat; :: thesis:
assume A474: n in dom h2 ; :: thesis:
reconsider m = ma + n, K2 = K2 as Nat ;
take m = m; :: thesis:
take K2 = K2; :: thesis:
ma + n in dom G1 by A469, A474;
hence ( [m,K2] in Indices G1 & h2 /. n = G1 * (m,K2) ) by A96, A365, A355, A421, A474, ZFMISC_1:87; :: thesis:

end;

A475: now :: thesis:

let n be Nat; :: thesis:
assume that
A476: n in dom h2 and
A477: n + 1 in dom h2 ; :: thesis:
ma + (n + 1) in dom G1 by A469, A477;
then A478: [((ma + n) + 1),K2] in Indices G1 by A96, A365, A355, ZFMISC_1:87;
let i1, i2, j1, j2 be Nat; :: thesis:
assume that
A479: [i1,i2] in Indices G1 and
A480: [j1,j2] in Indices G1 and
A481: h2 /. n = G1 * (i1,i2) and
A482: h2 /. (n + 1) = G1 * (j1,j2) ; :: thesis:
h2 /. (n + 1) = G1 * ((ma + (n + 1)),K2) by A421, A477;
then A483: ( j1 = (ma + n) + 1 & j2 = K2 ) by A478, A480, A482, GOBOARD1:5;
ma + n in dom G1 by A469, A476;
then A484: [(ma + n),K2] in Indices G1 by A96, A365, A355, ZFMISC_1:87;
h2 /. n = G1 * ((ma + n),K2) by A421, A476;
then ( i1 = ma + n & i2 = K2 ) by A484, A479, A481, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| = |.(((ma + n) - (ma + n)) + (- 1)).| + 0 by A483, ABSVALUE:2
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

A485: Seg (len h2) = dom h2 by FINSEQ_1:def 3;
A486: pl <= len (g2 | m) by A363, FINSEQ_3:25;
A487: 1 <= pl by A363, FINSEQ_3:25;
A488: pl <> pf by A39, A41, A95, A359, A363, GOBOARD1:3;

per cases by A488, XXREAL_0:1;

suppose pf < pl ; :: thesis:

then pf < len (g2 | m) by A486, XXREAL_0:2;
then 1 < len (g2 | m) by A364, XXREAL_0:2;
hence 1 + 1 <= len (g2 | m) by NAT_1:13; :: thesis:

end;

suppose pf > pl ; :: thesis:

then pl < len (g2 | m) by A418, XXREAL_0:2;
then 1 < len (g2 | m) by A487, XXREAL_0:2;
hence 1 + 1 <= len (g2 | m) by NAT_1:13; :: thesis:

end;

then 1 <= (len (g2 | m)) - 1 by XREAL_1:19;
then A489: lg in dom (g2 | m) by A356, FINSEQ_3:25;
A490: S₁₀[ 0 ] by FINSEQ_3:25;
A491: for n being Nat holds S₁₀[n] from NAT_1:sch 2(A490, A438);
A492: (rng h2) /\ (rng tt) = {}

end;

1 <= len (g2 | m) by A13, GOBOARD1:22;
then A506: len (g2 | m) in dom (g2 | m) by FINSEQ_3:25;
A507: dom (g2 | m) c= dom g2 by A23, A24, A16, A17, FINSEQ_1:5;

consider i2 being Element of NAT such that
A508: i2 in dom C and
A509: C /. i2 = (g2 | m) /. (len (g2 | m)) by A28, PARTFUN2:2;
A510: dom C = Seg (len C) by FINSEQ_1:def 3
.= Seg (len G1) by MATRIX_0:def 8
.= dom G1 by FINSEQ_1:def 3 ;
then A511: [i2,(width G1)] in Indices G1 by A73, A96, A508, ZFMISC_1:87;
C /. i2 = C . i2 by A508, PARTFUN1:def 6;
then A512: (g2 | m) /. (len (g2 | m)) = G1 * (i2,(width G1)) by A508, A509, A510, MATRIX_0:def 8;
assume A513: pl = len (g2 | m) ; :: thesis:
consider n1, n2 being Nat such that
A514: [n1,n2] in Indices G1 and
A515: (g2 | m) /. lg = G1 * (n1,n2) by A15, A489, GOBOARD1:def 9;
A516: n1 in dom G1 by A96, A514, ZFMISC_1:87;
A517: n2 in Seg (width G1) by A96, A514, ZFMISC_1:87;
[ma,K2] in Indices G1 by A41, A96, A365, A355, ZFMISC_1:87;
then i2 = ma by A420, A513, A512, A511, GOBOARD1:5;
then A518: |.(n1 - ma).| + |.(n2 - (width G1)).| = 1 by A15, A489, A506, A360, A512, A511, A514, A515, GOBOARD1:def 9;

per cases = 1 & n2 = width G1 ) or ( |.(n2 - (width G1)).| = 1 & n1 = ma ) ) by A518, SEQM_3:42;

suppose A519: ( |.(n1 - ma).| = 1 & n2 = width G1 ) ; :: thesis:

A520: dom C = Seg (len C) by FINSEQ_1:def 3
.= Seg (len G1) by MATRIX_0:def 8
.= dom G1 by FINSEQ_1:def 3 ;
then C /. n1 = C . n1 by A516, PARTFUN1:def 6;
then (g2 | m) /. lg = C /. n1 by A515, A516, A519, MATRIX_0:def 8;
then A521: (g2 | m) /. lg in rng C by A516, A520, PARTFUN2:2;
(g2 | m) /. lg = g2 /. lg by A13, A24, A17, A489, FINSEQ_4:71;
hence contradiction by A13, A17, A489, A507, A521, XREAL_1:44; :: thesis:

end;

suppose A522: ( |.(n2 - (width G1)).| = 1 & n1 = ma ) ; :: thesis:

len Lma = width G1 by MATRIX_0:def 7;
then A523: n2 in dom Lma by A517, FINSEQ_1:def 3;
then La /. n2 = Lma . n2 by PARTFUN1:def 6;
then (g2 | m) /. lg = Lma /. n2 by A515, A517, A522, MATRIX_0:def 7;
then (g2 | m) /. lg in rng Lma by A523, PARTFUN2:2;
hence contradiction by A363, A489, A513, XREAL_1:44; :: thesis:

end;

end;

then A524: pl < len (g2 | m) by A486, XXREAL_0:1;
len C = len G1 by MATRIX_0:def 8;
then A525: dom C = Seg (len G1) by FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3 ;
A526: Li /. K1 = Li . K1 by A367, PARTFUN1:def 6;
then A527: (g2 | m) /. pf = G1 * (mi,K1) by A367, A368, A400, MATRIX_0:def 7;

consider i2 being Element of NAT such that
A528: i2 in dom C and
A529: C /. i2 = (g2 | m) /. (len (g2 | m)) by A28, PARTFUN2:2;
C /. i2 = C . i2 by A528, PARTFUN1:def 6;
then A530: (g2 | m) /. (len (g2 | m)) = G1 * (i2,(width G1)) by A525, A528, A529, MATRIX_0:def 8;
A531: [i2,(width G1)] in Indices G1 by A73, A96, A525, A528, ZFMISC_1:87;
assume A532: pf = len (g2 | m) ; :: thesis:
consider n1, n2 being Nat such that
A533: [n1,n2] in Indices G1 and
A534: (g2 | m) /. lg = G1 * (n1,n2) by A15, A489, GOBOARD1:def 9;
A535: n1 in dom G1 by A96, A533, ZFMISC_1:87;
A536: n2 in Seg (width G1) by A96, A533, ZFMISC_1:87;
[mi,K1] in Indices G1 by A39, A96, A367, A400, ZFMISC_1:87;
then i2 = mi by A527, A532, A530, A531, GOBOARD1:5;
then A537: |.(n1 - mi).| + |.(n2 - (width G1)).| = 1 by A15, A489, A506, A360, A530, A531, A533, A534, GOBOARD1:def 9;

per cases = 1 & n2 = width G1 ) or ( |.(n2 - (width G1)).| = 1 & n1 = mi ) ) by A537, SEQM_3:42;

suppose A538: ( |.(n1 - mi).| = 1 & n2 = width G1 ) ; :: thesis:

A539: dom C = Seg (len C) by FINSEQ_1:def 3
.= Seg (len G1) by MATRIX_0:def 8
.= dom G1 by FINSEQ_1:def 3 ;
then C /. n1 = C . n1 by A535, PARTFUN1:def 6;
then (g2 | m) /. lg = C /. n1 by A534, A535, A538, MATRIX_0:def 8;
then A540: (g2 | m) /. lg in rng C by A535, A539, PARTFUN2:2;
(g2 | m) /. lg = g2 /. lg by A13, A24, A17, A489, FINSEQ_4:71;
hence contradiction by A13, A17, A489, A507, A540, XREAL_1:44; :: thesis:

end;

suppose A541: ( |.(n2 - (width G1)).| = 1 & n1 = mi ) ; :: thesis:

len Li = width G1 by MATRIX_0:def 7;
then A542: n2 in dom Li by A536, FINSEQ_1:def 3;
then Li /. n2 = Li . n2 by PARTFUN1:def 6;
then (g2 | m) /. lg = Li /. n2 by A534, A536, A541, MATRIX_0:def 7;
then (g2 | m) /. lg in rng Li by A542, PARTFUN2:2;
hence contradiction by A359, A489, A532, XREAL_1:44; :: thesis:

end;

end;

then A543: pf < len (g2 | m) by A418, XXREAL_0:1;

per cases by A488, XXREAL_0:1;

suppose A544: pf < pl ; :: thesis:

pl <= pl + 1 by NAT_1:11;
then reconsider LL = (pl + 1) - pf as Element of NAT by A544, INT_1:5, XXREAL_0:2;
reconsider w1 = pf - 1 as Element of NAT by A364, INT_1:5;
set F1 = (g2 | m) | pl;
defpred S₁₁[ Nat, Element of (TOP-REAL 2)] means $2 = ((g2 | m) | pl) /. (w1 + $1);
A545: for n being Nat st n in Seg LL holds
ex p being Point of (TOP-REAL 2) st S₁₁[n,p] ;
consider F being FinSequence of (TOP-REAL 2) such that
A546: ( len F = LL & ( for n being Nat st n in Seg LL holds
S₁₁[n,F /. n] ) ) from FINSEQ_4:sch 1(A545);
set hf = h1 ^ F;
set FF = (h1 ^ F) ^ h2;
A547: Seg (len F) = dom F by FINSEQ_1:def 3;
A548: for n being Nat st n in Seg LL holds
( ((g2 | m) | pl) /. (w1 + n) = (g2 | m) /. (w1 + n) & w1 + n in dom (g2 | m) )

let n be Nat; :: thesis:
assume A549: n in Seg LL ; :: thesis:
n <= LL by A549, FINSEQ_1:1;
then n + pf <= LL + pf by XREAL_1:7;
then A550: (n + pf) - 1 <= pl by XREAL_1:20;
1 <= n by A549, FINSEQ_1:1;
then 0 + 1 <= w1 + n by XREAL_1:7;
then w1 + n in Seg pl by A550, FINSEQ_1:1;
hence ( ((g2 | m) | pl) /. (w1 + n) = (g2 | m) /. (w1 + n) & w1 + n in dom (g2 | m) ) by A363, FINSEQ_4:71; :: thesis:

end;

A551: rng F c= rng g2

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng F ; :: thesis:
then consider n being Element of NAT such that
A552: n in dom F and
A553: x = F /. n by PARTFUN2:2;
F /. n = ((g2 | m) | pl) /. (w1 + n) by A546, A547, A552;
then A554: F /. n = (g2 | m) /. (w1 + n) by A548, A546, A547, A552;
w1 + n in dom (g2 | m) by A548, A546, A547, A552;
then x in rng (g2 | m) by A553, A554, PARTFUN2:2;
hence x in rng g2 by A18; :: thesis:

end;

pf + 1 <= pl by A544, NAT_1:13;
then pf + 1 <= pl + 1 by NAT_1:13;
then A555: 1 <= LL by XREAL_1:19;

A556: now :: thesis:

let i1, i2, j1, j2 be Nat; :: thesis:
assume that
A557: [i1,i2] in Indices G1 and
A558: [j1,j2] in Indices G1 and
A559: (h1 ^ F) /. (len (h1 ^ F)) = G1 * (i1,i2) and
A560: h2 /. 1 = G1 * (j1,j2) and
len (h1 ^ F) in dom (h1 ^ F) and
A561: 1 in dom h2 ; :: thesis:
ma + 1 in dom G1 by A469, A561;
then A562: [(ma + 1),K2] in Indices G1 by A96, A365, A355, ZFMISC_1:87;
A563: [ma,K2] in Indices G1 by A41, A96, A365, A355, ZFMISC_1:87;
A564: len F in dom F by A546, A547, A555, FINSEQ_1:1;
(h1 ^ F) /. (len (h1 ^ F)) = (h1 ^ F) /. ((len h1) + (len F)) by FINSEQ_1:22
.= F /. (len F) by A564, FINSEQ_4:69
.= ((g2 | m) | pl) /. (w1 + LL) by A546, A547, A564
.= G1 * (ma,K2) by A420, A548, A546, A547, A564 ;
then A565: ( i1 = ma & i2 = K2 ) by A557, A559, A563, GOBOARD1:5;
h2 /. 1 = G1 * ((ma + 1),K2) by A421, A561;
then ( j1 = ma + 1 & j2 = K2 ) by A558, A560, A562, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| = |.(ma - (ma + 1)).| + 0 by A565, ABSVALUE:2
.= |.(- ((ma + 1) - ma)).|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

A566: rng ((h1 ^ F) ^ h2) = (rng (h1 ^ F)) \/ (rng h2) by FINSEQ_1:31
.= ((rng h1) \/ (rng F)) \/ (rng h2) by FINSEQ_1:31 ;
A567: for k being Nat st k in Seg (width G1) & (rng F) /\ (rng (Col (G1,k))) = {} holds
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {}

A568: len (Col (G1,K2)) = len G1 by MATRIX_0:def 8;
A569: len (Col (G1,K1)) = len G1 by MATRIX_0:def 8;
let k be Nat; :: thesis:
assume that
A570: k in Seg (width G1) and
A571: (rng F) /\ (rng (Col (G1,k))) = {} ; :: thesis:
set gg = Col (G1,k);
assume A572: (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) <> {} ; :: thesis:
set x = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k)));
rng ((h1 ^ F) ^ h2) = (rng F) \/ ((rng h1) \/ (rng h2)) by A566, XBOOLE_1:4;
then A573: (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col (G1,k)))) by A571, XBOOLE_1:23
.= ((rng h1) /\ (rng (Col (G1,k)))) \/ ((rng h2) /\ (rng (Col (G1,k)))) by XBOOLE_1:23 ;

per cases by A572, A573, XBOOLE_0:def 3;

suppose A574: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k))) ; :: thesis:

then the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng h1 by XBOOLE_0:def 4;
then consider i being Element of NAT such that
A575: i in dom h1 and
A576: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = h1 /. i by PARTFUN2:2;
A577: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = G1 * (i,K1) by A369, A575, A576;
reconsider y = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) as Point of (TOP-REAL 2) by A576;
A578: Lmi /. K1 = Lmi . K1 by A367, PARTFUN1:def 6;
A579: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k)) by A574, XBOOLE_0:def 4;
A580: dom CK1 = Seg (len G1) by A569, FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3 ;
then A581: CK1 /. mi = CK1 . mi by A39, PARTFUN1:def 6;
A582: i in dom CK1 by A401, A575, A580;
CK1 /. i = CK1 . i by A401, A575, A580, PARTFUN1:def 6;
then y = CK1 /. i by A577, A580, A582, MATRIX_0:def 8;
then y in rng CK1 by A582, PARTFUN2:2;
then A583: K1 = k by A367, A400, A570, A579, GOBOARD1:4;
A584: 1 in Seg LL by A555, FINSEQ_1:1;
then ( F /. 1 = ((g2 | m) | pl) /. (w1 + 1) & ((g2 | m) | pl) /. (w1 + 1) = (g2 | m) /. (w1 + 1) ) by A548, A546;
then F /. 1 = CK1 /. mi by A39, A367, A368, A400, A578, A581, MATRIX_0:42;
then A585: F /. 1 in rng (Col (G1,k)) by A39, A580, A583, PARTFUN2:2;
F /. 1 in rng F by A546, A547, A584, PARTFUN2:2;
hence contradiction by A571, A585, XBOOLE_0:def 4; :: thesis:

end;

suppose A586: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k))) ; :: thesis:

then the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng h2 by XBOOLE_0:def 4;
then consider i being Element of NAT such that
A587: i in dom h2 and
A588: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = h2 /. i by PARTFUN2:2;
A589: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = G1 * ((ma + i),K2) by A421, A587, A588;
reconsider y = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) as Point of (TOP-REAL 2) by A588;
A590: Lma /. K2 = Lma . K2 by A365, PARTFUN1:def 6;
A591: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k)) by A586, XBOOLE_0:def 4;
A592: dom CK2 = Seg (len G1) by A568, FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3 ;
then A593: CK2 /. ma = CK2 . ma by A41, PARTFUN1:def 6;
A594: ma + i in dom CK2 by A469, A587, A592;
CK2 /. (ma + i) = CK2 . (ma + i) by A469, A587, A592, PARTFUN1:def 6;
then y = CK2 /. (ma + i) by A589, A592, A594, MATRIX_0:def 8;
then y in rng CK2 by A594, PARTFUN2:2;
then A595: K2 = k by A365, A355, A570, A591, GOBOARD1:4;
A596: LL in Seg LL by A555, FINSEQ_1:1;
then ( F /. LL = ((g2 | m) | pl) /. (w1 + LL) & ((g2 | m) | pl) /. (w1 + LL) = (g2 | m) /. (w1 + LL) ) by A548, A546;
then F /. LL = CK2 /. ma by A41, A365, A366, A355, A590, A593, MATRIX_0:42;
then A597: F /. LL in rng (Col (G1,k)) by A41, A592, A595, PARTFUN2:2;
F /. LL in rng F by A546, A547, A596, PARTFUN2:2;
hence contradiction by A571, A597, XBOOLE_0:def 4; :: thesis:

end;

end;

(rng F) /\ (rng C) = {}

reconsider w = w1 as Nat ;
set x = the Element of (rng F) /\ (rng C);
assume A598: not (rng F) /\ (rng C) = {} ; :: thesis:
then A599: the Element of (rng F) /\ (rng C) in rng C by XBOOLE_0:def 4;
the Element of (rng F) /\ (rng C) in rng F by A598, XBOOLE_0:def 4;
then consider i1 being Element of NAT such that
A600: i1 in dom F and
A601: F /. i1 = the Element of (rng F) /\ (rng C) by PARTFUN2:2;
A602: Seg (len F) = dom F by FINSEQ_1:def 3;
then i1 <= LL by A546, A600, FINSEQ_1:1;
then A603: w + i1 <= w + LL by XREAL_1:7;
A604: w1 + i1 in dom (g2 | m) by A548, A546, A600, A602;
then A605: w + i1 in dom g2 by A13, A24, A17, FINSEQ_4:71;
( F /. i1 = ((g2 | m) | pl) /. (w1 + i1) & ((g2 | m) | pl) /. (w1 + i1) = (g2 | m) /. (w1 + i1) ) by A548, A546, A600, A602;
then g2 /. (w + i1) in rng C by A13, A24, A17, A599, A601, A604, FINSEQ_4:71;
then m <= w + i1 by A13, A605;
hence contradiction by A17, A524, A603, XXREAL_0:2; :: thesis:

end;

then (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,(width G1)))) = {} by A73, A567;
then A606: rng ((h1 ^ F) ^ h2) misses rng (Col (G1,(width G1))) by XBOOLE_0:def 7;

reconsider w = w1 as Nat ;
let n be Nat; :: thesis:
assume A607: n in dom F ; :: thesis:
then w1 + n in dom (g2 | m) by A548, A546, A547;
then consider i, j being Nat such that
A608: ( [i,j] in Indices G1 & (g2 | m) /. (w + n) = G1 * (i,j) ) by A15, GOBOARD1:def 9;
take i = i; :: thesis:
take j = j; :: thesis:
F /. n = ((g2 | m) | pl) /. (w1 + n) by A546, A547, A607;
hence ( [i,j] in Indices G1 & F /. n = G1 * (i,j) ) by A548, A546, A547, A607, A608; :: thesis:

end;

then for n being Nat st n in dom (h1 ^ F) holds
ex i, j being Nat st
( [i,j] in Indices G1 & (h1 ^ F) /. n = G1 * (i,j) ) by A406, GOBOARD1:23;
then A609: for n being Nat st n in dom ((h1 ^ F) ^ h2) holds
ex i, j being Nat st
( [i,j] in Indices G1 & ((h1 ^ F) ^ h2) /. n = G1 * (i,j) ) by A473, GOBOARD1:23;

A610: now :: thesis:

A611: [mi,K1] in Indices G1 by A39, A96, A367, A400, ZFMISC_1:87;
let i1, i2, j1, j2 be Nat; :: thesis:
assume that
A612: [i1,i2] in Indices G1 and
A613: [j1,j2] in Indices G1 and
A614: h1 /. (len h1) = G1 * (i1,i2) and
A615: F /. 1 = G1 * (j1,j2) and
A616: len h1 in dom h1 and
A617: 1 in dom F ; :: thesis:
F /. 1 = ((g2 | m) | pl) /. (w1 + 1) by A546, A547, A617;
then F /. 1 = (g2 | m) /. (w1 + 1) by A548, A546, A547, A617
.= G1 * (mi,K1) by A367, A368, A400, A526, MATRIX_0:def 7 ;
then A618: ( j1 = mi & j2 = K1 ) by A613, A615, A611, GOBOARD1:5;
l1 in dom G1 by A369, A401, A616;
then A619: [l1,K1] in Indices G1 by A96, A367, A400, ZFMISC_1:87;
h1 /. (len h1) = G1 * (l1,K1) by A369, A616;
then ( i1 = l1 & i2 = K1 ) by A612, A614, A619, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| = |.((mi - 1) - mi).| + 0 by A618, ABSVALUE:2
.= |.(- 1).|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

let n be Nat; :: thesis:
assume that
A620: n in dom F and
A621: n + 1 in dom F ; :: thesis:
F /. n = ((g2 | m) | pl) /. (w1 + n) by A546, A547, A620;
then A622: F /. n = (g2 | m) /. (w1 + n) by A548, A546, A547, A620;
F /. (n + 1) = ((g2 | m) | pl) /. (w1 + (n + 1)) by A546, A547, A621;
then A623: ( (w1 + n) + 1 in dom (g2 | m) & F /. (n + 1) = (g2 | m) /. ((w1 + n) + 1) ) by A548, A546, A547, A621;
let i1, i2, j1, j2 be Nat; :: thesis:
assume A624: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) ) ; :: thesis:
w1 + n in dom (g2 | m) by A548, A546, A547, A620;
hence |.(i1 - j1).| + |.(i2 - j2).| = 1 by A15, A622, A623, A624, GOBOARD1:def 9; :: thesis:

end;

then for n being Nat st n in dom (h1 ^ F) & n + 1 in dom (h1 ^ F) holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ F) /. n = G1 * (i1,i2) & (h1 ^ F) /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 by A408, A610, GOBOARD1:24;
then for n being Nat st n in dom ((h1 ^ F) ^ h2) & n + 1 in dom ((h1 ^ F) ^ h2) holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & ((h1 ^ F) ^ h2) /. n = G1 * (i1,i2) & ((h1 ^ F) ^ h2) /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 by A475, A556, GOBOARD1:24;
then (h1 ^ F) ^ h2 is_sequence_on G1 by A609, GOBOARD1:def 9;
then A625: (h1 ^ F) ^ h2 is_sequence_on DelCol (G1,(width G1)) by A73, A152, A606, GOBOARD1:25;
set x = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng tt);
A626: 0 + 1 <= (len F) + ((len h1) + (len h2)) by A546, A555, XREAL_1:7;

A627: now :: thesis:

suppose A628: mi = 1 ; :: thesis:

A629: pf in Seg pl by A364, A544, FINSEQ_1:1;
A630: 1 in Seg LL by A555, FINSEQ_1:1;
h1 = {} by A369, A628;
then (h1 ^ F) ^ h2 = F ^ h2 by FINSEQ_1:34;
then ((h1 ^ F) ^ h2) /. 1 = F /. 1 by A546, A547, A630, FINSEQ_4:68
.= ((g2 | m) | pl) /. (w1 + 1) by A546, A630
.= (g2 | m) /. pf by A363, A629, FINSEQ_4:71 ;
hence ((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1)) by A359, A628; :: thesis:

end;

suppose A631: mi <> 1 ; :: thesis:

1 <= mi by A39, FINSEQ_3:25;
then 1 < mi by A631, XXREAL_0:1;
then 1 + 1 <= mi by NAT_1:13;
then A632: 1 <= l1 by XREAL_1:19;
then A633: 1 in Seg l1 by FINSEQ_1:1;
len (Line (G1,1)) = width G1 by MATRIX_0:def 7;
then A634: K1 in dom L1 by A367, A400, FINSEQ_1:def 3;
then A635: L1 /. K1 = L1 . K1 by PARTFUN1:def 6;
( len (h1 ^ F) = (len h1) + (len F) & 0 <= len F ) by FINSEQ_1:22;
then 0 + 1 <= len (h1 ^ F) by A369, A632, XREAL_1:7;
then 1 in dom (h1 ^ F) by FINSEQ_3:25;
then ((h1 ^ F) ^ h2) /. 1 = (h1 ^ F) /. 1 by FINSEQ_4:68
.= h1 /. 1 by A369, A468, A633, FINSEQ_4:68
.= G1 * (1,K1) by A369, A468, A633
.= L1 /. K1 by A367, A400, A635, MATRIX_0:def 7 ;
hence ((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1)) by A634, PARTFUN2:2; :: thesis:

end;

A636: w1 + LL = pl ;

A637: now :: thesis:

suppose A638: ma = len G1 ; :: thesis:

1 <= pl by A24, A363, FINSEQ_1:1;
then A639: pl in Seg pl by FINSEQ_1:1;
A640: len F in dom F by A546, A555, FINSEQ_3:25;
h2 = {} by A421, A638;
then A641: (h1 ^ F) ^ h2 = h1 ^ F by FINSEQ_1:34;
then ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) = ((h1 ^ F) ^ h2) /. ((len h1) + (len F)) by FINSEQ_1:22
.= F /. LL by A546, A641, A640, FINSEQ_4:69
.= ((g2 | m) | pl) /. pl by A546, A547, A636, A640
.= (g2 | m) /. pl by A363, A639, FINSEQ_4:71 ;
hence ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1))) by A363, A638; :: thesis:

end;

suppose A642: ma <> len G1 ; :: thesis:

ma <= len G1 by A41, FINSEQ_3:25;
then ma < len G1 by A642, XXREAL_0:1;
then ma + 1 <= len G1 by NAT_1:13;
then A643: 1 <= l2 by XREAL_1:19;
then A644: l2 in Seg l2 by FINSEQ_1:1;
len (Line (G1,(len G1))) = width G1 by MATRIX_0:def 7;
then A645: K2 in dom Ll by A365, A355, FINSEQ_1:def 3;
then A646: Ll /. K2 = Ll . K2 by PARTFUN1:def 6;
A647: len h2 in dom h2 by A421, A643, FINSEQ_3:25;
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) = ((h1 ^ F) ^ h2) /. ((len (h1 ^ F)) + (len h2)) by FINSEQ_1:22
.= h2 /. l2 by A421, A647, FINSEQ_4:69
.= G1 * ((ma + l2),K2) by A421, A485, A644
.= Ll /. K2 by A365, A355, A646, MATRIX_0:def 7 ;
hence ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line (G1,(len G1))) by A645, PARTFUN2:2; :: thesis:

end;

rng tt c= rng f by A351, A354;
then A648: rng tt c= rng g1 by A178;
A649: len ((h1 ^ F) ^ h2) = (len (h1 ^ F)) + (len h2) by FINSEQ_1:22
.= ((len h1) + (len F)) + (len h2) by FINSEQ_1:22 ;
then 1 in dom ((h1 ^ F) ^ h2) by A626, FINSEQ_3:25;
then A650: ((h1 ^ F) ^ h2) /. 1 in rng (Line ((DelCol (G1,(width G1))),1)) by A73, A26, A152, A627, A606, MATRIX_0:75;
len ((h1 ^ F) ^ h2) in dom ((h1 ^ F) ^ h2) by A649, A626, FINSEQ_3:25;
then A651: ((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) in rng (Line ((DelCol (G1,(width G1))),(len (DelCol (G1,(width G1)))))) by A73, A27, A152, A153, A637, A606, MATRIX_0:75;
width (DelCol (G1,(width G1))) = k by A3, A73, MATRIX_0:63;
then (rng ((h1 ^ F) ^ h2)) /\ (rng tt) <> {} by A2, A92, A353, A649, A626, A625, A650, A651, A341;
then A652: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng tt) in (rng ((h1 ^ F) ^ h2)) /\ (rng tt) ;
(rng tt) /\ (rng ((h1 ^ F) ^ h2)) = (((rng h1) \/ (rng F)) /\ (rng tt)) \/ {} by A492, A566, XBOOLE_1:23
.= {} \/ ((rng F) /\ (rng tt)) by A424, XBOOLE_1:23
.= (rng tt) /\ (rng F) ;
then (rng ((h1 ^ F) ^ h2)) /\ (rng tt) c= (rng g1) /\ (rng g2) by A648, A551, XBOOLE_1:27;
hence (rng g1) /\ (rng g2) <> {} by A652; :: thesis:

end;

suppose A653: pl < pf ; :: thesis:

pf <= pf + 1 by NAT_1:11;
then reconsider LL = (pf + 1) - pl as Element of NAT by A653, INT_1:5, XXREAL_0:2;
set F1 = (g2 | m) | pf;
defpred S₁₁[ Nat, Element of (TOP-REAL 2)] means for k being Nat st k = (pf + 1) - $1 holds
$2 = ((g2 | m) | pf) /. k;
A654: for n, k being Nat st n in Seg LL & k = (pf + 1) - n holds
( ((g2 | m) | pf) /. k = (g2 | m) /. k & k in dom (g2 | m) )

let n, k be Nat; :: thesis:
assume that
A655: n in Seg LL and
A656: k = (pf + 1) - n ; :: thesis:
A657: n <= LL by A655, FINSEQ_1:1;
1 <= n by A655, FINSEQ_1:1;
then A658: (pf + 1) - n <= (pf + 1) - 1 by XREAL_1:13;
LL <= (pf + 1) - 0 by XREAL_1:13;
then reconsider w = (pf + 1) - n as Element of NAT by A657, INT_1:5, XXREAL_0:2;
(pf + 1) - LL <= (pf + 1) - n by A657, XREAL_1:13;
then 1 <= (pf + 1) - n by A487, XXREAL_0:2;
then w in Seg pf by A658, FINSEQ_1:1;
hence ( ((g2 | m) | pf) /. k = (g2 | m) /. k & k in dom (g2 | m) ) by A359, A656, FINSEQ_4:71; :: thesis:

end;

A659: for n being Nat st n in Seg LL holds
(pf + 1) - n is Element of NAT

let n be Nat; :: thesis:
A660: LL <= (pf + 1) - 0 by XREAL_1:13;
assume n in Seg LL ; :: thesis:
then n <= LL by FINSEQ_1:1;
hence (pf + 1) - n is Element of NAT by A660, INT_1:5, XXREAL_0:2; :: thesis:

end;

A661: for n being Nat st n in Seg LL holds
ex p being Point of (TOP-REAL 2) st S₁₁[n,p]

let n be Nat; :: thesis:
assume A662: n in Seg LL ; :: thesis:
then reconsider k = (pf + 1) - n as Nat by A659;
take (g2 | m) /. k ; :: thesis:
thus S₁₁[n,(g2 | m) /. k] by A654, A662; :: thesis:

end;

consider F being FinSequence of (TOP-REAL 2) such that
A663: ( len F = LL & ( for n being Nat st n in Seg LL holds
S₁₁[n,F /. n] ) ) from FINSEQ_4:sch 1(A661);
set hf = h1 ^ F;
set FF = (h1 ^ F) ^ h2;
A664: Seg (len F) = dom F by FINSEQ_1:def 3;
A665: rng F c= rng g2

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng F ; :: thesis:
then consider n being Element of NAT such that
A666: n in dom F and
A667: x = F /. n by PARTFUN2:2;
reconsider u = (pf + 1) - n as Nat by A659, A663, A664, A666;
F /. n = ((g2 | m) | pf) /. u by A663, A664, A666;
then ( (pf + 1) - n in dom (g2 | m) & F /. n = (g2 | m) /. u ) by A654, A663, A664, A666;
then x in rng (g2 | m) by A667, PARTFUN2:2;
hence x in rng g2 by A18; :: thesis:

end;

pl + 1 <= pf by A653, NAT_1:13;
then pl + 1 <= pf + 1 by NAT_1:13;
then A668: 1 <= LL by XREAL_1:19;

A669: now :: thesis:

reconsider u = (pf + 1) - LL as Nat ;
let i1, i2, j1, j2 be Nat; :: thesis:
assume that
A670: [i1,i2] in Indices G1 and
A671: [j1,j2] in Indices G1 and
A672: (h1 ^ F) /. (len (h1 ^ F)) = G1 * (i1,i2) and
A673: h2 /. 1 = G1 * (j1,j2) and
len (h1 ^ F) in dom (h1 ^ F) and
A674: 1 in dom h2 ; :: thesis:
ma + 1 in dom G1 by A469, A674;
then A675: [(ma + 1),K2] in Indices G1 by A96, A365, A355, ZFMISC_1:87;
A676: [ma,K2] in Indices G1 by A41, A96, A365, A355, ZFMISC_1:87;
A677: len F in dom F by A663, A668, FINSEQ_3:25;
(h1 ^ F) /. (len (h1 ^ F)) = (h1 ^ F) /. ((len h1) + (len F)) by FINSEQ_1:22
.= F /. (len F) by A677, FINSEQ_4:69
.= ((g2 | m) | pf) /. u by A663, A664, A677
.= (g2 | m) /. u by A654, A663, A664, A677
.= G1 * (ma,K2) by A365, A366, A355, A419, MATRIX_0:def 7 ;
then A678: ( i1 = ma & i2 = K2 ) by A670, A672, A676, GOBOARD1:5;
h2 /. 1 = G1 * ((ma + 1),K2) by A421, A674;
then ( j1 = ma + 1 & j2 = K2 ) by A671, A673, A675, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| = |.(ma - (ma + 1)).| + 0 by A678, ABSVALUE:2
.= |.(- ((ma + 1) - ma)).|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

let n be Nat; :: thesis:
assume A679: n in dom F ; :: thesis:
then reconsider w = (pf + 1) - n as Nat by A659, A663, A664;
A680: F /. n = ((g2 | m) | pf) /. w by A663, A664, A679;
then (pf + 1) - n in dom (g2 | m) by A654, A663, A664, A679;
then consider i, j being Nat such that
A681: ( [i,j] in Indices G1 & (g2 | m) /. w = G1 * (i,j) ) by A15, GOBOARD1:def 9;
take i = i; :: thesis:
take j = j; :: thesis:
thus ( [i,j] in Indices G1 & F /. n = G1 * (i,j) ) by A654, A663, A664, A679, A680, A681; :: thesis:

end;

then for n being Nat st n in dom (h1 ^ F) holds
ex i, j being Nat st
( [i,j] in Indices G1 & (h1 ^ F) /. n = G1 * (i,j) ) by A406, GOBOARD1:23;
then A682: for n being Nat st n in dom ((h1 ^ F) ^ h2) holds
ex i, j being Nat st
( [i,j] in Indices G1 & ((h1 ^ F) ^ h2) /. n = G1 * (i,j) ) by A473, GOBOARD1:23;
set x = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng tt);
A683: 0 + 1 <= (len F) + ((len h1) + (len h2)) by A663, A668, XREAL_1:7;
A684: rng ((h1 ^ F) ^ h2) = (rng (h1 ^ F)) \/ (rng h2) by FINSEQ_1:31
.= ((rng h1) \/ (rng F)) \/ (rng h2) by FINSEQ_1:31 ;
A685: for k being Nat st k in Seg (width G1) & (rng F) /\ (rng (Col (G1,k))) = {} holds
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {}

A686: len (Col (G1,K2)) = len G1 by MATRIX_0:def 8;
A687: len (Col (G1,K1)) = len G1 by MATRIX_0:def 8;
let k be Nat; :: thesis:
assume that
A688: k in Seg (width G1) and
A689: (rng F) /\ (rng (Col (G1,k))) = {} ; :: thesis:
set gg = Col (G1,k);
assume A690: (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) <> {} ; :: thesis:
set x = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k)));
rng ((h1 ^ F) ^ h2) = (rng F) \/ ((rng h1) \/ (rng h2)) by A684, XBOOLE_1:4;
then A691: (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = {} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col (G1,k)))) by A689, XBOOLE_1:23
.= ((rng h1) /\ (rng (Col (G1,k)))) \/ ((rng h2) /\ (rng (Col (G1,k)))) by XBOOLE_1:23 ;

per cases by A690, A691, XBOOLE_0:def 3;

suppose A692: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h1) /\ (rng (Col (G1,k))) ; :: thesis:

then A693: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k)) by XBOOLE_0:def 4;
A694: 1 in Seg LL by A668, FINSEQ_1:1;
(pf + 1) - 1 = pf ;
then A695: ( F /. 1 = ((g2 | m) | pf) /. pf & ((g2 | m) | pf) /. pf = (g2 | m) /. pf ) by A654, A663, A694;
the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng h1 by A692, XBOOLE_0:def 4;
then consider i being Element of NAT such that
A696: i in dom h1 and
A697: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = h1 /. i by PARTFUN2:2;
A698: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = G1 * (i,K1) by A369, A696, A697;
reconsider y = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) as Point of (TOP-REAL 2) by A697;
A699: Lmi /. K1 = Lmi . K1 by A367, PARTFUN1:def 6;
A700: dom CK1 = Seg (len G1) by A687, FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3 ;
then A701: i in dom CK1 by A401, A696;
CK1 /. i = CK1 . i by A401, A696, A700, PARTFUN1:def 6;
then y = CK1 /. i by A698, A700, A701, MATRIX_0:def 8;
then y in rng CK1 by A701, PARTFUN2:2;
then A702: K1 = k by A367, A400, A688, A693, GOBOARD1:4;
CK1 /. mi = CK1 . mi by A39, A700, PARTFUN1:def 6;
then F /. 1 = CK1 /. mi by A39, A367, A368, A400, A699, A695, MATRIX_0:42;
then A703: F /. 1 in rng (Col (G1,k)) by A39, A700, A702, PARTFUN2:2;
F /. 1 in rng F by A663, A664, A694, PARTFUN2:2;
hence contradiction by A689, A703, XBOOLE_0:def 4; :: thesis:

end;

suppose A704: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in (rng h2) /\ (rng (Col (G1,k))) ; :: thesis:

then the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng h2 by XBOOLE_0:def 4;
then consider i being Element of NAT such that
A705: i in dom h2 and
A706: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = h2 /. i by PARTFUN2:2;
A707: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) = G1 * ((ma + i),K2) by A421, A705, A706;
reconsider y = the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) as Point of (TOP-REAL 2) by A706;
A708: the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,k))) in rng (Col (G1,k)) by A704, XBOOLE_0:def 4;
reconsider u = (pf + 1) - LL as Nat ;
A709: Lma /. K2 = Lma . K2 by A365, PARTFUN1:def 6;
A710: dom CK2 = Seg (len G1) by A686, FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3 ;
then A711: CK2 /. ma = CK2 . ma by A41, PARTFUN1:def 6;
A712: ma + i in dom CK2 by A469, A705, A710;
CK2 /. (ma + i) = CK2 . (ma + i) by A469, A705, A710, PARTFUN1:def 6;
then y = CK2 /. (ma + i) by A707, A710, A712, MATRIX_0:def 8;
then y in rng CK2 by A712, PARTFUN2:2;
then A713: K2 = k by A365, A355, A688, A708, GOBOARD1:4;
A714: LL in Seg LL by A668, FINSEQ_1:1;
then ( F /. LL = ((g2 | m) | pf) /. u & ((g2 | m) | pf) /. u = (g2 | m) /. u ) by A654, A663;
then F /. LL = CK2 /. ma by A41, A365, A366, A355, A709, A711, MATRIX_0:42;
then A715: F /. LL in rng (Col (G1,k)) by A41, A710, A713, PARTFUN2:2;
F /. LL in rng F by A663, A664, A714, PARTFUN2:2;
hence contradiction by A689, A715, XBOOLE_0:def 4; :: thesis:

end;

end;

(rng F) /\ (rng C) = {}

set x = the Element of (rng F) /\ (rng C);
assume A716: not (rng F) /\ (rng C) = {} ; :: thesis:
then A717: the Element of (rng F) /\ (rng C) in rng C by XBOOLE_0:def 4;
the Element of (rng F) /\ (rng C) in rng F by A716, XBOOLE_0:def 4;
then consider i1 being Element of NAT such that
A718: i1 in dom F and
A719: F /. i1 = the Element of (rng F) /\ (rng C) by PARTFUN2:2;
reconsider w = (pf + 1) - i1 as Nat by A659, A663, A664, A718;
1 <= i1 by A718, FINSEQ_3:25;
then A720: w <= (pf + 1) - 1 by XREAL_1:13;
A721: w in dom (g2 | m) by A654, A663, A664, A718;
then A722: w in dom g2 by A13, A24, A17, FINSEQ_4:71;
( F /. i1 = ((g2 | m) | pf) /. w & ((g2 | m) | pf) /. w = (g2 | m) /. w ) by A654, A663, A664, A718;
then g2 /. w in rng C by A13, A24, A17, A717, A719, A721, FINSEQ_4:71;
then m <= w by A13, A722;
hence contradiction by A17, A543, A720, XXREAL_0:2; :: thesis:

end;

then (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (G1,(width G1)))) = {} by A73, A685;
then A723: rng ((h1 ^ F) ^ h2) misses rng (Col (G1,(width G1))) by XBOOLE_0:def 7;

A724: now :: thesis:

let n be Nat; :: thesis:
assume that
A725: n in dom F and
A726: n + 1 in dom F ; :: thesis:
reconsider w3 = (pf + 1) - n, w2 = (pf + 1) - (n + 1) as Element of NAT by A659, A663, A664, A725, A726;
F /. n = ((g2 | m) | pf) /. w3 by A663, A664, A725;
then A727: ( (pf + 1) - n in dom (g2 | m) & F /. n = (g2 | m) /. w3 ) by A654, A663, A664, A725;
F /. (n + 1) = ((g2 | m) | pf) /. w2 by A663, A664, A726;
then A728: ( (pf + 1) - (n + 1) in dom (g2 | m) & F /. (n + 1) = (g2 | m) /. w2 ) by A654, A663, A664, A726;
let i1, i2, j1, j2 be Nat; :: thesis:
assume A729: ( [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & F /. n = G1 * (i1,i2) & F /. (n + 1) = G1 * (j1,j2) ) ; :: thesis:
w2 + 1 = (pf + 1) - n ;
hence 1 = |.(j1 - i1).| + |.(j2 - i2).| by A15, A727, A728, A729, GOBOARD1:def 9
.= |.(- (i1 - j1)).| + |.(- (i2 - j2)).|
.= |.(i1 - j1).| + |.(- (i2 - j2)).| by COMPLEX1:52
.= |.(i1 - j1).| + |.(i2 - j2).| by COMPLEX1:52 ;
:: thesis:

end;

A730: (pf + 1) - 1 = pf ;

A731: now :: thesis:

suppose A732: mi = 1 ; :: thesis:

A733: pf in Seg pf by A364, FINSEQ_1:1;
A734: 1 in Seg LL by A668, FINSEQ_1:1;
h1 = {} by A369, A732;
then (h1 ^ F) ^ h2 = F ^ h2 by FINSEQ_1:34;
then ((h1 ^ F) ^ h2) /. 1 = F /. 1 by A663, A664, A734, FINSEQ_4:68
.= ((g2 | m) | pf) /. pf by A663, A730, A734
.= (g2 | m) /. pf by A359, A733, FINSEQ_4:71 ;
hence ((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1)) by A359, A732; :: thesis:

end;

suppose A735: mi <> 1 ; :: thesis:

1 <= mi by A39, FINSEQ_3:25;
then 1 < mi by A735, XXREAL_0:1;
then 1 + 1 <= mi by NAT_1:13;
then A736: 1 <= l1 by XREAL_1:19;
then A737: 1 in Seg l1 by FINSEQ_1:1;
len (Line (G1,1)) = width G1 by MATRIX_0:def 7;
then A738: K1 in dom L1 by A367, A400, FINSEQ_1:def 3;
then A739: L1 /. K1 = L1 . K1 by PARTFUN1:def 6;
( len (h1 ^ F) = (len h1) + (len F) & 0 <= len F ) by FINSEQ_1:22;
then 0 + 1 <= len (h1 ^ F) by A369, A736, XREAL_1:7;
then 1 in dom (h1 ^ F) by FINSEQ_3:25;
then ((h1 ^ F) ^ h2) /. 1 = (h1 ^ F) /. 1 by FINSEQ_4:68
.= h1 /. 1 by A369, A468, A737, FINSEQ_4:68
.= G1 * (1,K1) by A369, A468, A737
.= L1 /. K1 by A367, A400, A739, MATRIX_0:def 7 ;
hence ((h1 ^ F) ^ h2) /. 1 in rng (Line (G1,1)) by A738, PARTFUN2:2; :: thesis:

end;

rng tt c= rng f by A351, A354;
then A740: rng tt c= rng g1 by A178;

A741: [mi,K1] in Indices G1 by A39, A96, A367, A400, ZFMISC_1:87;
reconsider w4 = (pf + 1) - 1 as Nat ;
let i1, i2, j1, j2 be Nat; :: thesis:
assume that
A742: [i1,i2] in Indices G1 and
A743: [j1,j2] in Indices G1 and
A744: h1 /. (len h1) = G1 * (i1,i2) and
A745: F /. 1 = G1 * (j1,j2) and
A746: len h1 in dom h1 and
A747: 1 in dom F ; :: thesis:
F /. 1 = ((g2 | m) | pf) /. w4 by A663, A664, A747
.= (g2 | m) /. w4 by A654, A663, A664, A747
.= G1 * (mi,K1) by A367, A368, A400, A526, MATRIX_0:def 7 ;
then A748: ( j1 = mi & j2 = K1 ) by A743, A745, A741, GOBOARD1:5;
l1 in dom G1 by A369, A401, A746;
then A749: [l1,K1] in Indices G1 by A96, A367, A400, ZFMISC_1:87;
h1 /. (len h1) = G1 * (l1,K1) by A369, A746;
then ( i1 = l1 & i2 = K1 ) by A742, A744, A749, GOBOARD1:5;
hence |.(i1 - j1).| + |.(i2 - j2).| = |.((mi - 1) - mi).| + 0 by A748, ABSVALUE:2
.= |.(- 1).|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1 ;
:: thesis:

end;

then for n being Nat st n in dom (h1 ^ F) & n + 1 in dom (h1 ^ F) holds
for i1, i2, j1, j2 being Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1 ^ F) /. n = G1 * (i1,i2) & (h1 ^ F) /. (n + 1) = G1 * (j1,j2) holds
|.(i1 - j1).| + |.(i2 - j2).| = 1 by A408, A724, GOBOARD1:24;
then for n being Nat st n in dom ((h1 ^ F) ^ h2) & n + 1 in dom ((h1 ^ F) ^ h2) holds
for m, k, i, j being Nat st [m,k] in Indices G1 & [i,j] in Indices G1 & ((h1 ^ F) ^ h2) /. n = G1 * (m,k) & ((h1 ^ F) ^ h2) /. (n + 1) = G1 * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 by A475, A669, GOBOARD1:24;
then (h1 ^ F) ^ h2 is_sequence_on G1 by A682, GOBOARD1:def 9;
then A750: (h1 ^ F) ^ h2 is_sequence_on DelCol (G1,(width G1)) by A73, A152, A723, GOBOARD1:25;
A751: len ((h1 ^ F) ^ h2) = (len (h1 ^ F)) + (len h2) by FINSEQ_1:22
.= ((len h1) + (len F)) + (len h2) by FINSEQ_1:22 ;
then 1 in dom ((h1 ^ F) ^ h2) by A683, FINSEQ_3:25;
then A752: ((h1 ^ F) ^ h2) /. 1 in rng (Line ((DelCol (G1,(width G1))),1)) by A73, A26, A152, A731, A723, MATRIX_0:75;

A753: now :: thesis: