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, Th7; :: 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;
A25: len (Line G,j) = m + 1 by A3, MATRIX_1:def 8;
thus (Col N,k) . j = N * j,k by A24, MATRIX_1:def 9
.= (Del (Line G,j),i) . k by A4, A11, A12, A13, A19, A24
.= (Line G,j) . k by A23, A25, 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 A26: 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 A27: j in dom N by A22, FINSEQ_3:27;
A28: len (Line G,j) = m + 1 by A3, MATRIX_1:def 8;
A29: dom (Line G,j) = Seg (len (Line G,j)) by FINSEQ_1:def 3;
thus (Col N,k) . j = N * j,k by A27, MATRIX_1:def 9
.= (Del (Line G,j),i) . k by A4, A11, A12, A13, A19, A27
.= (Line G,j) . (k + 1) by A1, A3, A20, A26, A28, A29, FINSEQ_3:120
.= (Col G,(k + 1)) . j by A4, A11, A12, A21, A27, 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 A30: ( 0 < len M & 0 < width M ) by A2, MATRIX_1:24;

A31: now

let k be Element of NAT ; :: thesis: ( k in dom M implies X_axis (Line M,k) is constant )
assume A32: k in dom M ; :: thesis: X_axis (Line M,k) is constant
then A33: X_axis (Line G,k) is constant by A4, A11, A12, Def6;
m <= m + 1 by NAT_1:11;
then A34: 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 A35: ( n in dom (X_axis L) & j in dom (X_axis L) ) ; :: thesis: (X_axis L) . n = (X_axis L) . j
A36: ( 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 A37: ( L . n = M * k,n & L . j = M * k,j & n in Seg m & j in Seg m ) by A2, A35, MATRIX_1:24, MATRIX_1:def 8;
then A38: ( ( 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, A32;
( n in dom L & j in dom L ) by A35, A36, FINSEQ_1:def 3;
then ( L . n = L /. n & L . j = L /. j ) by PARTFUN1:def 8;
then A39: ( (X_axis L) . n = (M * k,n) `1 & (X_axis L) . j = (M * k,j) `1 ) by A35, A37, Def3;
( 1 <= n & n <= m & 1 <= j & j <= m ) by A12, A35, A36, FINSEQ_3:27;
then A40: ( 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 A41: ( 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, A34, A35, A36, A40, FINSEQ_3:27;
then A42: ( 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 A36, 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 A36, A41, 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 A36, A41, A42, Def3;
hence (X_axis L) . n = (X_axis L) . j by A33, A36, A37, A38, A39, A41, A42, Def2; :: thesis: verum

end;

hence X_axis (Line M,k) is constant by Def2; :: thesis: verum

end;

A43: now

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

end;

A47: 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 A48: Seg m c= Seg (width G) by A3, FINSEQ_1:7;
assume A49: k in dom M ; :: thesis: Y_axis (Line M,k) is increasing
then A50: 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 A51: ( n in dom (Y_axis L) & j in dom (Y_axis L) & n < j ) ; :: thesis: (Y_axis L) . b₁ < (Y_axis L) . b₂
A52: ( 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 A53: ( L . n = M * k,n & L . j = M * k,j & n in Seg m & j in Seg m ) by A2, A51, MATRIX_1:24, MATRIX_1:def 8;
dom L = Seg (len (Y_axis L)) by A52, FINSEQ_1:def 3;
then ( L . n = L /. n & L . j = L /. j ) by A51, A52, PARTFUN1:def 8;
then A54: ( (Y_axis L) . n = (M * k,n) `2 & (Y_axis L) . j = (M * k,j) `2 ) by A51, A53, Def4;
A55: ( 1 <= n & n <= m & 1 <= j & j <= m ) by A12, A51, A52, FINSEQ_3:27;
then A56: ( 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 A57: ( 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, A48, A51, A52, A56, FINSEQ_3:27;
then A58: ( 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 A52, 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 A52, A57, PARTFUN1:def 8;
then A59: ( (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 A52, A57, A58, Def4;
set r = (Y_axis L) . n;
set s = (Y_axis L) . j;
A60: dom lg = Seg (len lg) by FINSEQ_1:def 3;

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

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

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

end;

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

A65: M * k,j = (Del lg,i) . j by A4, A11, A12, A13, A49, A51, A52
.= G * k,(j + 1) by A1, A3, A52, A55, A58, A60, A64, FINSEQ_3:120 ;

now

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

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

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

end;

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

A69: n + 1 < j + 1 by A51, XREAL_1:8;
M * k,n = (Del lg,i) . n by A4, A11, A12, A13, A49, A51, A52
.= G * k,(n + 1) by A1, A3, A52, A55, A58, A60, A68, FINSEQ_3:120 ;
hence (Y_axis L) . n < (Y_axis L) . j by A50, A52, A54, A57, A59, A65, A69, 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 A70: k in Seg (width M) ; :: thesis: X_axis (Col M,k) is increasing
then A71: ( Col M,k = Col G,k or Col M,k = Col G,(k + 1) ) by A12, A18;
A72: ( 1 <= k & k <= m ) by A12, A70, 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 A72, XREAL_1:8, XXREAL_0:2;
then ( k in Seg (width G) & k + 1 in Seg (width G) ) by A3, A72, FINSEQ_1:3;
hence X_axis (Col M,k) is increasing by A71, 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 A30, A31, A43, A47, 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 A73: 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 A74: k in dom G ; :: thesis: M . k = Del (Line G,k),i
then A75: M . k = Line M,k by A4, A11, A73, MATRIX_2:18;
then reconsider s = M . k as FinSequence ;
A76: len s = m by A12, A75, MATRIX_1:def 8;
A77: len (Del (Line G,k),i) = m by A5, A74;
X: dom s = Seg m by A76, 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, X, MATRIX_1:def 8;
hence s . j = (Del (Line G,k),i) . j by A13, A74, A75, A78, X; :: thesis: verum

end;

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