defpred S₁[ Nat, Nat, Point of (TOP-REAL 2)] means $3 = (Del ((Line (G,$1)),i)) . $2;
A2: ( 0 < len G & 0 < width G ) by Lm1;
then consider m being Nat such that
A3: width G = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A4: Seg (len G) = dom G by FINSEQ_1:def 3;
A5: for k being Element of NAT st k in dom G holds
len (Del ((Line (G,k)),i)) = m

proof

let k be Element of NAT ; :: thesis: ( k in dom G implies len (Del ((Line (G,k)),i)) = m )
assume k in dom G ; :: thesis: len (Del ((Line (G,k)),i)) = m
A6: len (Line (G,k)) = width G by MATRIX_1:def 8;
then i in dom (Line (G,k)) by A1, FINSEQ_1:def 3;
then ex j being Nat st
( len (Line (G,k)) = j + 1 & len (Del ((Line (G,k)),i)) = j ) by FINSEQ_3:113;
hence len (Del ((Line (G,k)),i)) = m by A3, A6; :: thesis: verum

end;

A7: for k, j being Nat st [k,j] in [:(Seg (len G)),(Seg m):] holds
for x1, x2 being Point of (TOP-REAL 2) st S₁[k,j,x1] & S₁[k,j,x2] holds
x1 = x2 ;
A8: for k, j being Nat st [k,j] in [:(Seg (len G)),(Seg m):] holds
ex x being Point of (TOP-REAL 2) st S₁[k,j,x]

proof

let k, j be Nat; :: thesis: ( [k,j] in [:(Seg (len G)),(Seg m):] implies ex x being Point of (TOP-REAL 2) st S₁[k,j,x] )
assume [k,j] in [:(Seg (len G)),(Seg m):] ; :: thesis: ex x being Point of (TOP-REAL 2) st S₁[k,j,x]
then A9: ( k in dom G & j in Seg m ) by A4, ZFMISC_1:106;
reconsider p = Del ((Line (G,k)),i) as FinSequence of (TOP-REAL 2) by FINSEQ_3:114;
len p = m by A5, A9;
then j in dom p by A9, FINSEQ_1:def 3;
then reconsider x = p . j as Point of (TOP-REAL 2) by FINSEQ_2:13;
take x ; :: thesis: S₁[k,j,x]
thus S₁[k,j,x] ; :: thesis: verum

end;

consider N being Matrix of len G,m, the carrier of (TOP-REAL 2) such that
A10: for k, j being Nat st [k,j] in Indices N holds
S₁[k,j,N * (k,j)] from MATRIX_1:sch 2(A7, A8);
A11: Seg (len N) = dom N by FINSEQ_1:def 3;
A12: ( len N = len G & width N = m & Indices N = [:(dom G),(Seg m):] ) by A2, A4, MATRIX_1:24;
A13: for k, j being Element of NAT st k in dom G & j in Seg m holds
N * (k,j) = (Del ((Line (G,k)),i)) . j

proof

let k, j be Element of NAT ; :: thesis: ( k in dom G & j in Seg m implies N * (k,j) = (Del ((Line (G,k)),i)) . j )
assume ( k in dom G & j in Seg m ) ; :: thesis: N * (k,j) = (Del ((Line (G,k)),i)) . j
then [k,j] in Indices N by A12, ZFMISC_1:106;
hence N * (k,j) = (Del ((Line (G,k)),i)) . j by A10; :: thesis: verum

end;

A14: for k, j being Element of NAT st k in dom G & j in Seg m & not N * (k,j) = (Line (G,k)) . j holds
N * (k,j) = (Line (G,k)) . (j + 1)

proof

let k, j be Element of NAT ; :: thesis: ( k in dom G & j in Seg m & not N * (k,j) = (Line (G,k)) . j implies N * (k,j) = (Line (G,k)) . (j + 1) )
assume A15: ( k in dom G & j in Seg m ) ; :: thesis: ( N * (k,j) = (Line (G,k)) . j or N * (k,j) = (Line (G,k)) . (j + 1) )
then A16: N * (k,j) = (Del ((Line (G,k)),i)) . j by A13;
A17: len (Line (G,k)) = m + 1 by A3, MATRIX_1:def 8;
i in Seg (len (Line (G,k))) by A1, MATRIX_1:def 8;
then i in dom (Line (G,k)) by FINSEQ_1:def 3;
hence ( N * (k,j) = (Line (G,k)) . j or N * (k,j) = (Line (G,k)) . (j + 1) ) by A15, A16, A17, SEQM_3:84; :: thesis: verum

end;

A18: for k being Element of NAT holds
( not k in Seg m or Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) )

proof

let k be Element of NAT ; :: thesis: ( not k in Seg m or Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) )
assume A19: k in Seg m ; :: thesis: ( Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) )
then A20: ( 1 <= k & k <= m ) by FINSEQ_1:3;
( m <= m + 1 & k <= k + 1 ) by NAT_1:11;
then ( k <= m + 1 & 1 <= k + 1 & k + 1 <= m + 1 ) by A20, XREAL_1:8, XXREAL_0:2;
then A21: ( k in Seg (width G) & k + 1 in Seg (width G) ) by A3, A20, FINSEQ_1:3;
A22: ( len (Col (N,k)) = len N & len (Col (G,k)) = len G & len (Col (G,(k + 1))) = len G ) by MATRIX_1:def 9;

now

per cases ( k < i or k >= i ) ;

suppose A23: k < i ; :: thesis: ( Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) )

now

let j be Nat; :: thesis: ( 1 <= j & j <= len (Col (N,k)) implies (Col (N,k)) . j = (Col (G,k)) . j )
assume ( 1 <= j & j <= len (Col (N,k)) ) ; :: thesis: (Col (N,k)) . j = (Col (G,k)) . j
then A24: j in dom N by A22, FINSEQ_3:27;
hence (Col (N,k)) . j = N * (j,k) by MATRIX_1:def 9
.= (Del ((Line (G,j)),i)) . k by A4, A11, A12, A13, A19, A24
.= (Line (G,j)) . k by A23, FINSEQ_3:119
.= (Col (G,k)) . j by A4, A11, A12, A21, A24, Th17 ;
:: thesis: verum

end;

hence ( Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) ) by A12, A22, FINSEQ_1:18; :: thesis: verum

end;

suppose A25: k >= i ; :: thesis: ( Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) )

now

let j be Nat; :: thesis: ( 1 <= j & j <= len (Col (N,k)) implies (Col (N,k)) . j = (Col (G,(k + 1))) . j )
assume ( 1 <= j & j <= len (Col (N,k)) ) ; :: thesis: (Col (N,k)) . j = (Col (G,(k + 1))) . j
then A26: j in dom N by A22, FINSEQ_3:27;
A27: len (Line (G,j)) = m + 1 by A3, MATRIX_1:def 8;
A28: dom (Line (G,j)) = Seg (len (Line (G,j))) by FINSEQ_1:def 3;
thus (Col (N,k)) . j = N * (j,k) by A26, MATRIX_1:def 9
.= (Del ((Line (G,j)),i)) . k by A4, A11, A12, A13, A19, A26
.= (Line (G,j)) . (k + 1) by A1, A3, A20, A25, A27, A28, FINSEQ_3:120
.= (Col (G,(k + 1))) . j by A4, A11, A12, A21, A26, Th17 ; :: thesis: verum

end;

hence ( Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) ) by A12, A22, FINSEQ_1:18; :: thesis: verum

end;

end;

end;

hence ( Col (N,k) = Col (G,k) or Col (N,k) = Col (G,(k + 1)) ) ; :: thesis: verum

end;

reconsider M = N as Matrix of (TOP-REAL 2) ;
1 - 1 < m by A1, A3, XREAL_1:21;
then A29: ( 0 < len M & 0 < width M ) by A2, MATRIX_1:24;

A30: now

let k be Element of NAT ; :: thesis: ( k in dom M implies X_axis (Line (M,k)) is constant )
assume A31: k in dom M ; :: thesis: X_axis (Line (M,k)) is constant
then A32: X_axis (Line (G,k)) is constant by A4, A11, A12, Def6;
m <= m + 1 by NAT_1:11;
then A33: Seg m c= Seg (width G) by A3, FINSEQ_1:7;
reconsider L = Line (M,k), lg = Line (G,k) as FinSequence of (TOP-REAL 2) ;
set X = X_axis L;
set xg = X_axis lg;

now

let n, j be Element of NAT ; :: thesis: ( n in dom (X_axis L) & j in dom (X_axis L) implies (X_axis L) . n = (X_axis L) . j )
assume A34: ( n in dom (X_axis L) & j in dom (X_axis L) ) ; :: thesis: (X_axis L) . n = (X_axis L) . j
A35: ( dom (X_axis L) = Seg (len (X_axis L)) & len (X_axis L) = len L & len L = width M & dom (X_axis lg) = Seg (len (X_axis lg)) & len (X_axis lg) = len lg & len lg = width G ) by Def3, FINSEQ_1:def 3, MATRIX_1:def 8;
then A36: ( L . n = M * (k,n) & L . j = M * (k,j) & n in Seg m & j in Seg m ) by A2, A34, MATRIX_1:24, MATRIX_1:def 8;
then A37: ( ( L . n = lg . n or L . n = lg . (n + 1) ) & ( L . j = lg . j or L . j = lg . (j + 1) ) ) by A4, A11, A12, A14, A31;
( n in dom L & j in dom L ) by A34, A35, FINSEQ_1:def 3;
then ( L . n = L /. n & L . j = L /. j ) by PARTFUN1:def 8;
then A38: ( (X_axis L) . n = (M * (k,n)) `1 & (X_axis L) . j = (M * (k,j)) `1 ) by A34, A36, Def3;
( 1 <= n & n <= m & 1 <= j & j <= m ) by A12, A34, A35, FINSEQ_3:27;
then A39: ( n <= n + 1 & n + 1 <= m + 1 & j <= j + 1 & j + 1 <= m + 1 ) by NAT_1:11, XREAL_1:8;
( 1 <= n + 1 & 1 <= j + 1 ) by NAT_1:11;
then A40: ( n + 1 in Seg (width G) & j + 1 in Seg (width G) & n in Seg (width G) & j in Seg (width G) ) by A3, A12, A33, A34, A35, A39, FINSEQ_3:27;
then A41: ( lg . n = G * (k,n) & lg . (n + 1) = G * (k,(n + 1)) & lg . j = G * (k,j) & lg . (j + 1) = G * (k,(j + 1)) ) by MATRIX_1:def 8;
dom lg = Seg (len (X_axis lg)) by A35, FINSEQ_1:def 3;
then ( lg . n = lg /. n & lg . (n + 1) = lg /. (n + 1) & lg . j = lg /. j & lg . (j + 1) = lg /. (j + 1) ) by A35, A40, PARTFUN1:def 8;
then ( (X_axis lg) . n = (G * (k,n)) `1 & (X_axis lg) . (n + 1) = (G * (k,(n + 1))) `1 & (X_axis lg) . j = (G * (k,j)) `1 & (X_axis lg) . (j + 1) = (G * (k,(j + 1))) `1 ) by A35, A40, A41, Def3;
hence (X_axis L) . n = (X_axis L) . j by A32, A35, A36, A37, A38, A40, A41, SEQM_3:def 15; :: thesis: verum

end;

hence X_axis (Line (M,k)) is constant by SEQM_3:def 15; :: thesis: verum

end;

A42: now

let k be Element of NAT ; :: thesis: ( k in Seg (width M) implies Y_axis (Col (M,k)) is constant )
assume A43: k in Seg (width M) ; :: thesis: Y_axis (Col (M,k)) is constant
then A44: ( Col (M,k) = Col (G,k) or Col (M,k) = Col (G,(k + 1)) ) by A12, A18;
A45: ( 1 <= k & k <= m ) by A12, A43, FINSEQ_1:3;
( m <= m + 1 & k <= k + 1 ) by NAT_1:11;
then ( k <= m + 1 & 1 <= k + 1 & k + 1 <= m + 1 ) by A45, XREAL_1:8, XXREAL_0:2;
then ( k in Seg (width G) & k + 1 in Seg (width G) ) by A3, A45, FINSEQ_1:3;
hence Y_axis (Col (M,k)) is constant by A44, Def7; :: thesis: verum

end;

A46: now

let k be Element of NAT ; :: thesis: ( k in dom M implies Y_axis (Line (M,k)) is increasing )
reconsider L = Line (M,k), lg = Line (G,k) as FinSequence of (TOP-REAL 2) ;
set X = Y_axis L;
set xg = Y_axis lg;
m <= m + 1 by NAT_1:11;
then A47: Seg m c= Seg (width G) by A3, FINSEQ_1:7;
assume A48: k in dom M ; :: thesis: Y_axis (Line (M,k)) is increasing
then A49: Y_axis lg is increasing by A4, A11, A12, Def8;

now

let n, j be Element of NAT ; :: thesis: ( n in dom (Y_axis L) & j in dom (Y_axis L) & n < j implies (Y_axis L) . b₁ < (Y_axis L) . b₂ )
assume A50: ( n in dom (Y_axis L) & j in dom (Y_axis L) & n < j ) ; :: thesis: (Y_axis L) . b₁ < (Y_axis L) . b₂
A51: ( dom (Y_axis L) = Seg (len (Y_axis L)) & len (Y_axis L) = len L & len L = width M & dom (Y_axis lg) = Seg (len (Y_axis lg)) & len (Y_axis lg) = len lg & len lg = width G ) by Def4, FINSEQ_1:def 3, MATRIX_1:def 8;
then A52: ( L . n = M * (k,n) & L . j = M * (k,j) & n in Seg m & j in Seg m ) by A2, A50, MATRIX_1:24, MATRIX_1:def 8;
dom L = Seg (len (Y_axis L)) by A51, FINSEQ_1:def 3;
then ( L . n = L /. n & L . j = L /. j ) by A50, A51, PARTFUN1:def 8;
then A53: ( (Y_axis L) . n = (M * (k,n)) `2 & (Y_axis L) . j = (M * (k,j)) `2 ) by A50, A52, Def4;
A54: ( 1 <= n & n <= m & 1 <= j & j <= m ) by A12, A50, A51, FINSEQ_3:27;
then A55: ( n <= n + 1 & n + 1 <= m + 1 & j <= j + 1 & j + 1 <= m + 1 ) by NAT_1:11, XREAL_1:8;
( 1 <= n + 1 & 1 <= j + 1 ) by NAT_1:11;
then A56: ( n + 1 in Seg (width G) & j + 1 in Seg (width G) & n in Seg (width G) & j in Seg (width G) ) by A3, A12, A47, A50, A51, A55, FINSEQ_3:27;
then A57: ( lg . n = G * (k,n) & lg . (n + 1) = G * (k,(n + 1)) & lg . j = G * (k,j) & lg . (j + 1) = G * (k,(j + 1)) ) by MATRIX_1:def 8;
dom lg = Seg (len (Y_axis lg)) by A51, FINSEQ_1:def 3;
then ( lg . n = lg /. n & lg . (n + 1) = lg /. (n + 1) & lg . j = lg /. j & lg . (j + 1) = lg /. (j + 1) ) by A51, A56, PARTFUN1:def 8;
then A58: ( (Y_axis lg) . n = (G * (k,n)) `2 & (Y_axis lg) . (n + 1) = (G * (k,(n + 1))) `2 & (Y_axis lg) . j = (G * (k,j)) `2 & (Y_axis lg) . (j + 1) = (G * (k,(j + 1))) `2 ) by A51, A56, A57, Def4;
set r = (Y_axis L) . n;
set s = (Y_axis L) . j;
A59: dom lg = Seg (len lg) by FINSEQ_1:def 3;

per cases ( j < i or j >= i ) ;

suppose A60: j < i ; :: thesis: (Y_axis L) . b₁ < (Y_axis L) . b₂

then A61: n < i by A50, XXREAL_0:2;
A62: M * (k,n) = (Del (lg,i)) . n by A4, A11, A12, A13, A48, A50, A51
.= G * (k,n) by A57, A61, FINSEQ_3:119 ;
M * (k,j) = (Del (lg,i)) . j by A4, A11, A12, A13, A48, A50, A51
.= G * (k,j) by A57, A60, FINSEQ_3:119 ;
hence (Y_axis L) . n < (Y_axis L) . j by A12, A47, A49, A50, A51, A53, A58, A62, SEQM_3:def 1; :: thesis: verum

end;

suppose A63: j >= i ; :: thesis: (Y_axis L) . b₁ < (Y_axis L) . b₂

A64: M * (k,j) = (Del (lg,i)) . j by A4, A11, A12, A13, A48, A50, A51
.= G * (k,(j + 1)) by A1, A3, A51, A54, A57, A59, A63, FINSEQ_3:120 ;

now

per cases ( n < i or n >= i ) ;

suppose A65: n < i ; :: thesis: (Y_axis L) . n < (Y_axis L) . j

j <= j + 1 by NAT_1:11;
then A66: n < j + 1 by A50, XXREAL_0:2;
M * (k,n) = (Del (lg,i)) . n by A4, A11, A12, A13, A48, A50, A51
.= G * (k,n) by A57, A65, FINSEQ_3:119 ;
hence (Y_axis L) . n < (Y_axis L) . j by A49, A51, A53, A56, A58, A64, A66, SEQM_3:def 1; :: thesis: verum

end;

suppose A67: n >= i ; :: thesis: (Y_axis L) . n < (Y_axis L) . j

A68: n + 1 < j + 1 by A50, XREAL_1:8;
M * (k,n) = (Del (lg,i)) . n by A4, A11, A12, A13, A48, A50, A51
.= G * (k,(n + 1)) by A1, A3, A51, A54, A57, A59, A67, FINSEQ_3:120 ;
hence (Y_axis L) . n < (Y_axis L) . j by A49, A51, A53, A56, A58, A64, A68, SEQM_3:def 1; :: thesis: verum

end;

end;

end;

hence (Y_axis L) . n < (Y_axis L) . j ; :: thesis: verum

end;

end;

end;

hence Y_axis (Line (M,k)) is increasing by SEQM_3:def 1; :: thesis: verum

end;

now

let k be Element of NAT ; :: thesis: ( k in Seg (width M) implies X_axis (Col (M,k)) is increasing )
assume A69: k in Seg (width M) ; :: thesis: X_axis (Col (M,k)) is increasing
then A70: ( Col (M,k) = Col (G,k) or Col (M,k) = Col (G,(k + 1)) ) by A12, A18;
A71: ( 1 <= k & k <= m ) by A12, A69, FINSEQ_1:3;
( m <= m + 1 & k <= k + 1 ) by NAT_1:11;
then ( k <= m + 1 & 1 <= k + 1 & k + 1 <= m + 1 ) by A71, XREAL_1:8, XXREAL_0:2;
then ( k in Seg (width G) & k + 1 in Seg (width G) ) by A3, A71, FINSEQ_1:3;
hence X_axis (Col (M,k)) is increasing by A70, Def9; :: thesis: verum

end;

then reconsider M = M as V3() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column Matrix of (TOP-REAL 2) by A29, A30, A42, A46, Def5, Def6, Def7, Def8, Def9;
take M ; :: thesis: ( len M = len G & ( for k being Element of NAT st k in dom G holds
M . k = Del ((Line (G,k)),i) ) )
thus A72: len M = len G by A2, MATRIX_1:24; :: thesis: for k being Element of NAT st k in dom G holds
M . k = Del ((Line (G,k)),i)
let k be Element of NAT ; :: thesis: ( k in dom G implies M . k = Del ((Line (G,k)),i) )
assume A73: k in dom G ; :: thesis: M . k = Del ((Line (G,k)),i)
then A74: M . k = Line (M,k) by A4, A11, A72, MATRIX_2:18;
then reconsider s = M . k as FinSequence ;
A75: len s = m by A12, A74, MATRIX_1:def 8;
A76: len (Del ((Line (G,k)),i)) = m by A5, A73;
A77: dom s = Seg m by A75, FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom s implies s . j = (Del ((Line (G,k)),i)) . j )
assume A78: j in dom s ; :: thesis: s . j = (Del ((Line (G,k)),i)) . j
then (Line (M,k)) . j = M * (k,j) by A12, A77, MATRIX_1:def 8;
hence s . j = (Del ((Line (G,k)),i)) . j by A13, A73, A74, A78, A77; :: thesis: verum

end;

hence M . k = Del ((Line (G,k)),i) by A75, A76, FINSEQ_2:10; :: thesis: verum