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