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) and
A2: x in rng (Line M,m) and
A3: n in dom M and
A4: m in dom M and
A5: n <> m ;
A6: ( n < m or m < n ) by A5, XXREAL_0:1;
A7: X_axis (Line M,m) is constant by A4, Def6;
reconsider Ln = Line M,n, Lm = Line M,m as FinSequence of (TOP-REAL 2) ;
consider i being Nat such that
A8: i in dom Ln and
A9: Ln . i = x by A1, FINSEQ_2:11;
set C = X_axis (Col M,i);
A10: len Ln = width M by MATRIX_1:def 8;
reconsider Mi = Col M,i as FinSequence of (TOP-REAL 2) ;
A11: (Col M,i) . n = M * n,i by A3, MATRIX_1:def 9;
A12: len (Col M,i) = len M by MATRIX_1:def 9;
then n in dom (Col M,i) by A3, FINSEQ_3:31;
then A13: M * n,i = Mi /. n by A11, PARTFUN1:def 8;
A14: (Col M,i) . m = M * m,i by A4, MATRIX_1:def 9;
A15: dom M = Seg (len M) by FINSEQ_1:def 3;
then m in dom (Col M,i) by A4, A12, FINSEQ_1:def 3;
then A16: M * m,i = Mi /. m by A14, PARTFUN1:def 8;
consider j being Nat such that
A17: j in dom Lm and
A18: Lm . j = x by A2, FINSEQ_2:11;
A19: ( len (X_axis (Col M,i)) = len (Col M,i) & dom (X_axis (Col M,i)) = Seg (len (X_axis (Col M,i))) ) by Def3, FINSEQ_1:def 3;
A20: Seg (len Ln) = dom Ln by FINSEQ_1:def 3;
then A21: X_axis (Col M,i) is increasing by A8, A10, Def9;
A22: len Lm = width M by MATRIX_1:def 8;
then A23: i in dom Lm by A8, A10, FINSEQ_3:31;
Lm . i = M * m,i by A8, A10, A20, MATRIX_1:def 8;
then A24: Lm /. i = M * m,i by A23, PARTFUN1:def 8;
A25: dom (X_axis Lm) = Seg (len (X_axis Lm)) by FINSEQ_1:def 3;
Ln . i = M * n,i by A8, A10, A20, MATRIX_1:def 8;
then reconsider p = x as Point of (TOP-REAL 2) by A9;
A26: Lm /. j = p by A17, A18, PARTFUN1:def 8;
A27: len (X_axis Lm) = len Lm by Def3;
then A28: j in dom (X_axis Lm) by A17, FINSEQ_3:31;
Seg (len Lm) = dom Lm by FINSEQ_1:def 3;
then A29: j in dom (X_axis Lm) by A17, A25, Def3;
i in dom (X_axis Lm) by A8, A10, A22, A27, FINSEQ_3:31;
then (X_axis Lm) . i = (X_axis Lm) . j by A7, A28, Def2;
then A30: (M * m,i) `1 = (X_axis Lm) . j by A8, A25, A10, A22, A27, A20, A24, Def3
.= p `1 by A29, A26, Def3 ;
(M * n,i) `1 = p `1 by A8, A9, A10, A20, MATRIX_1:def 8;
then (X_axis (Col M,i)) . n = p `1 by A3, A15, A12, A19, A13, Def3
.= (X_axis (Col M,i)) . m by A4, A15, A12, A19, A30, A16, Def3 ;
hence contradiction by A3, A4, A15, A21, A12, A19, A6, SEQM_3:def 1; :: thesis: verum