let M be X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2); :: thesis: for x being set
for n, m being Element of NAT st x in rng (Line M,n) & x in rng (Line M,m) & n in dom M & m in dom M holds
n = m
assume ex x being set ex n, m being Element of NAT st
( x in rng (Line M,n) & x in rng (Line M,m) & n in dom M & m in dom M & not n = m ) ; :: thesis: contradiction
then consider x being set , n, m being Element of NAT such that
A1: ( x in rng (Line M,n) & x in rng (Line M,m) & n in dom M & m in dom M & n <> m ) ;
A2: X_axis (Line M,m) is constant by A1, Def6;
reconsider Ln = Line M,n, Lm = Line 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 Mi = Col 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 (X_axis Ln) = Seg (len (X_axis Ln)) & dom (X_axis Lm) = Seg (len (X_axis Lm)) & len Ln = width M & len Lm = width M ) by FINSEQ_1:def 3, MATRIX_1:def 8;
set C = X_axis (Col M,i);
A6: ( len (X_axis Ln) = len Ln & len (X_axis Lm) = len Lm ) by Def3;
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: ( X_axis (Col M,i) is increasing & len (X_axis (Col M,i)) = len (Col M,i) & len (Col M,i) = len M & dom (X_axis (Col M,i)) = Seg (len (X_axis (Col M,i))) ) by A3, A5, Def3, Def9, FINSEQ_1:def 3, MATRIX_1:def 9;
A10: ( Lm . i = M * m,i & Ln . i = M * n,i & Lm . j = M * m,j & (Col M,i) . n = M * n,i & (Col M,i) . m = M * m,i ) by A1, A3, A4, A5, 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 (X_axis Lm) & j in dom (X_axis Lm) ) by A3, A4, A5, A8, Def3;
i in dom Lm by A3, A5, FINSEQ_3:31;
then A12: Lm /. i = M * m,i by A10, PARTFUN1:def 8;
A13: Lm /. j = p by A4, PARTFUN1:def 8;
( i in dom (X_axis Lm) & j in dom (X_axis Lm) ) by A3, A4, A5, A6, FINSEQ_3:31;
then (X_axis Lm) . i = (X_axis Lm) . j by A2, Def2;
then A14: (M * m,i) `1 = (X_axis Lm) . j by A3, A5, A6, A8, A12, Def3
.= p `1 by A11, A13, Def3 ;
A15: (M * n,i) `1 = p `1 by A3, A5, A8, MATRIX_1:def 8;
m in dom (Col M,i) by A1, A7, A9, FINSEQ_1:def 3;
then A16: M * m,i = Mi /. m by A10, PARTFUN1:def 8;
n in dom (Col M,i) by A1, A9, FINSEQ_3:31;
then M * n,i = Mi /. n by A10, PARTFUN1:def 8;
then A17: (X_axis (Col M,i)) . n = p `1 by A1, A7, A9, A15, Def3
.= (X_axis (Col M,i)) . m by A1, A7, A9, A14, A16, Def3 ;
( n < m or m < n ) by A1, XXREAL_0:1;
hence contradiction by A1, A7, A9, A17, SEQM_3:def 1; :: thesis: verum