let M be Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2); :: thesis: for x being set
for n, m being Element of NAT st x in rng (Col M,n) & x in rng (Col M,m) & n in Seg (width M) & m in Seg (width M) holds
n = m
assume ex x being set ex n, m being Element of NAT st
( x in rng (Col M,n) & x in rng (Col M,m) & n in Seg (width M) & m in Seg (width M) & not n = m ) ; :: thesis: contradiction
then consider x being set , n, m being Element of NAT such that
A1: ( x in rng (Col M,n) & x in rng (Col M,m) & n in Seg (width M) & m in Seg (width M) & n <> m ) ;
A2: Y_axis (Col M,m) is constant by A1, Def7;
reconsider Ln = Col M,n, Lm = Col M,m as FinSequence of (TOP-REAL 2) ;
consider i being Nat such that
A3: ( i in dom Ln & Ln . i = x ) by A1, FINSEQ_2:11;
reconsider Li = Line M,i as FinSequence of (TOP-REAL 2) ;
consider j being Nat such that
A4: ( j in dom Lm & Lm . j = x ) by A1, FINSEQ_2:11;
A5: ( dom (Y_axis Ln) = Seg (len (Y_axis Ln)) & dom (Y_axis Lm) = Seg (len (Y_axis Lm)) & len Ln = len M & len Lm = len M ) by FINSEQ_1:def 3, MATRIX_1:def 9;
set C = Y_axis (Line M,i);
A6: ( len (Y_axis Ln) = len Ln & len (Y_axis Lm) = len Lm ) by Def4;
A7: dom M = Seg (len M) by FINSEQ_1:def 3;
A8: ( Seg (len Ln) = dom Ln & Seg (len Lm) = dom Lm ) by FINSEQ_1:def 3;
then A9: ( Y_axis (Line M,i) is increasing & len (Y_axis (Line M,i)) = len (Line M,i) & len (Line M,i) = width M & dom (Y_axis (Line M,i)) = Seg (len (Y_axis (Line M,i))) ) by A3, A5, A7, Def4, Def8, FINSEQ_1:def 3, MATRIX_1:def 8;
A10: ( Lm . i = M * i,m & Ln . i = M * i,n & Lm . j = M * j,m & (Line M,i) . n = M * i,n & (Line M,i) . m = M * i,m ) by A1, A3, A4, A5, A7, A8, MATRIX_1:def 8, MATRIX_1:def 9;
then reconsider p = x as Point of (TOP-REAL 2) by A3;
A11: ( i in dom (Y_axis Lm) & j in dom (Y_axis Lm) ) by A3, A4, A5, A8, Def4;
i in dom Lm by A3, A5, FINSEQ_3:31;
then A12: Lm /. i = M * i,m by A10, PARTFUN1:def 8;
A13: Lm /. j = p by A4, PARTFUN1:def 8;
(Y_axis Lm) . i = (Y_axis Lm) . j by A2, A3, A4, A5, A6, A8, Def2;
then A14: (M * i,m) `2 = (Y_axis Lm) . j by A3, A5, A6, A8, A12, Def4
.= p `2 by A11, A13, Def4 ;
A15: (M * i,n) `2 = p `2 by A3, A5, A7, A8, MATRIX_1:def 9;
m in dom (Line M,i) by A1, A9, FINSEQ_1:def 3;
then A16: M * i,m = Li /. m by A10, PARTFUN1:def 8;
n in dom (Line M,i) by A1, A9, FINSEQ_1:def 3;
then M * i,n = Li /. n by A10, PARTFUN1:def 8;
then A17: (Y_axis (Line M,i)) . n = p `2 by A1, A9, A15, Def4
.= (Y_axis (Line M,i)) . m by A1, A9, A14, A16, Def4 ;
( n < m or m < n ) by A1, XXREAL_0:1;
hence contradiction by A1, A9, A17, SEQM_3:def 1; :: thesis: verum