let M be X_equal-in-line X_increasing-in-column Matrix of (); :: 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 ;
A7: X_axis (Line (M,m)) is constant by ;
reconsider Ln = Line (M,n), Lm = Line (M,m) as FinSequence of () ;
consider i being Nat such that
A8: i in dom Ln and
A9: Ln . i = x by ;
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 () ;
A11: (Col (M,i)) . n = M * (n,i) by ;
A12: len (Col (M,i)) = len M by MATRIX_0:def 8;
then n in dom (Col (M,i)) by ;
then A13: M * (n,i) = Mi /. n by ;
A14: (Col (M,i)) . m = M * (m,i) by ;
A15: dom M = Seg (len M) by FINSEQ_1:def 3;
then m in dom (Col (M,i)) by ;
then A16: M * (m,i) = Mi /. m by ;
consider j being Nat such that
A17: j in dom Lm and
A18: Lm . j = x by ;
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 ;
A20: Seg (len Ln) = dom Ln by FINSEQ_1:def 3;
then A21: X_axis (Col (M,i)) is increasing by ;
A22: len Lm = width M by MATRIX_0:def 7;
then A23: i in dom Lm by ;
Lm . i = M * (m,i) by ;
then A24: Lm /. i = M * (m,i) by ;
A25: dom (X_axis Lm) = Seg (len (X_axis Lm)) by FINSEQ_1:def 3;
Ln . i = M * (n,i) by ;
then reconsider p = x as Point of () by A9;
A26: Lm /. j = p by ;
A27: len (X_axis Lm) = len Lm by Def1;
then A28: j in dom (X_axis Lm) by ;
Seg (len Lm) = dom Lm by FINSEQ_1:def 3;
then A29: j in dom (X_axis Lm) by ;
i in dom (X_axis Lm) by ;
then (X_axis Lm) . i = (X_axis Lm) . j by ;
then A30: (M * (m,i)) `1 = (X_axis Lm) . j by A8, A25, A10, A22, A27, A20, A24, Def1
.= p `1 by ;
(M * (n,i)) `1 = p `1 by ;
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