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 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 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 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, Def3;

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:10;

set C = X_axis (Col (M,i));

A10: len Ln = width M by MATRIX_0:def 7;

reconsider Mi = Col (M,i) as FinSequence of (TOP-REAL 2) ;

A11: (Col (M,i)) . n = M * (n,i) by A3, MATRIX_0:def 8;

A12: len (Col (M,i)) = len M by MATRIX_0:def 8;

then n in dom (Col (M,i)) by A3, FINSEQ_3:29;

then A13: M * (n,i) = Mi /. n by A11, PARTFUN1:def 6;

A14: (Col (M,i)) . m = M * (m,i) by A4, MATRIX_0:def 8;

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 6;

consider j being Nat such that

A17: j in dom Lm and

A18: Lm . j = x by A2, FINSEQ_2:10;

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 Def1, 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, Def6;

A22: len Lm = width M by MATRIX_0:def 7;

then A23: i in dom Lm by A8, A10, FINSEQ_3:29;

Lm . i = M * (m,i) by A8, A10, A20, MATRIX_0:def 7;

then A24: Lm /. i = M * (m,i) by A23, PARTFUN1:def 6;

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_0:def 7;

then reconsider p = x as Point of (TOP-REAL 2) by A9;

A26: Lm /. j = p by A17, A18, PARTFUN1:def 6;

A27: len (X_axis Lm) = len Lm by Def1;

then A28: j in dom (X_axis Lm) by A17, FINSEQ_3:29;

Seg (len Lm) = dom Lm by FINSEQ_1:def 3;

then A29: j in dom (X_axis Lm) by A17, A25, Def1;

i in dom (X_axis Lm) by A8, A10, A22, A27, FINSEQ_3:29;

then (X_axis Lm) . i = (X_axis Lm) . j by A7, A28;

then A30: (M * (m,i)) `1 = (X_axis Lm) . j by A8, A25, A10, A22, A27, A20, A24, Def1

.= p `1 by A29, A26, Def1 ;

(M * (n,i)) `1 = p `1 by A8, A9, A10, A20, MATRIX_0:def 7;

then (X_axis (Col (M,i))) . n = p `1 by A3, A15, A12, A19, A13, Def1

.= (X_axis (Col (M,i))) . m by A4, A15, A12, A19, A30, A16, Def1 ;

hence contradiction by A3, A4, A15, A21, A12, A19, A6; :: thesis: verum

for n, m being 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 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 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, Def3;

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:10;

set C = X_axis (Col (M,i));

A10: len Ln = width M by MATRIX_0:def 7;

reconsider Mi = Col (M,i) as FinSequence of (TOP-REAL 2) ;

A11: (Col (M,i)) . n = M * (n,i) by A3, MATRIX_0:def 8;

A12: len (Col (M,i)) = len M by MATRIX_0:def 8;

then n in dom (Col (M,i)) by A3, FINSEQ_3:29;

then A13: M * (n,i) = Mi /. n by A11, PARTFUN1:def 6;

A14: (Col (M,i)) . m = M * (m,i) by A4, MATRIX_0:def 8;

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 6;

consider j being Nat such that

A17: j in dom Lm and

A18: Lm . j = x by A2, FINSEQ_2:10;

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 Def1, 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, Def6;

A22: len Lm = width M by MATRIX_0:def 7;

then A23: i in dom Lm by A8, A10, FINSEQ_3:29;

Lm . i = M * (m,i) by A8, A10, A20, MATRIX_0:def 7;

then A24: Lm /. i = M * (m,i) by A23, PARTFUN1:def 6;

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_0:def 7;

then reconsider p = x as Point of (TOP-REAL 2) by A9;

A26: Lm /. j = p by A17, A18, PARTFUN1:def 6;

A27: len (X_axis Lm) = len Lm by Def1;

then A28: j in dom (X_axis Lm) by A17, FINSEQ_3:29;

Seg (len Lm) = dom Lm by FINSEQ_1:def 3;

then A29: j in dom (X_axis Lm) by A17, A25, Def1;

i in dom (X_axis Lm) by A8, A10, A22, A27, FINSEQ_3:29;

then (X_axis Lm) . i = (X_axis Lm) . j by A7, A28;

then A30: (M * (m,i)) `1 = (X_axis Lm) . j by A8, A25, A10, A22, A27, A20, A24, Def1

.= p `1 by A29, A26, Def1 ;

(M * (n,i)) `1 = p `1 by A8, A9, A10, A20, MATRIX_0:def 7;

then (X_axis (Col (M,i))) . n = p `1 by A3, A15, A12, A19, A13, Def1

.= (X_axis (Col (M,i))) . m by A4, A15, A12, A19, A30, A16, Def1 ;

hence contradiction by A3, A4, A15, A21, A12, A19, A6; :: thesis: verum