let n, m be Nat; :: thesis: for K being Field
for M being Matrix of m,n,K
for i being Nat
for a being Element of K st ( for j being Nat st j in Seg m holds
M * j,i = a ) holds
( M is without_repeated_line iff Segm M,(Seg (len M)),((Seg (width M)) \ {i}) is without_repeated_line )
let K be Field; :: thesis: for M being Matrix of m,n,K
for i being Nat
for a being Element of K st ( for j being Nat st j in Seg m holds
M * j,i = a ) holds
( M is without_repeated_line iff Segm M,(Seg (len M)),((Seg (width M)) \ {i}) is without_repeated_line )
let M be Matrix of m,n,K; :: thesis: for i being Nat
for a being Element of K st ( for j being Nat st j in Seg m holds
M * j,i = a ) holds
( M is without_repeated_line iff Segm M,(Seg (len M)),((Seg (width M)) \ {i}) is without_repeated_line )
let i be Nat; :: thesis: for a being Element of K st ( for j being Nat st j in Seg m holds
M * j,i = a ) holds
( M is without_repeated_line iff Segm M,(Seg (len M)),((Seg (width M)) \ {i}) is without_repeated_line )
let a be Element of K; :: thesis: ( ( for j being Nat st j in Seg m holds
M * j,i = a ) implies ( M is without_repeated_line iff Segm M,(Seg (len M)),((Seg (width M)) \ {i}) is without_repeated_line ) )
assume A1: for j being Nat st j in Seg m holds
M * j,i = a ; :: thesis: ( M is without_repeated_line iff Segm M,(Seg (len M)),((Seg (width M)) \ {i}) is without_repeated_line )
set SMi = (Seg (width M)) \ {i};
set S = Segm M,(Seg (len M)),((Seg (width M)) \ {i});
set Si = Sgm ((Seg (width M)) \ {i});
set Sl = Sgm (Seg (len M));
A2: ( len M = m & len (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) = card (Seg (len M)) & card (Seg (len M)) = len M ) by FINSEQ_1:78, MATRIX_1:def 3;
then A3: ( dom M = Seg m & dom (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) = Seg m ) by FINSEQ_1:def 3;
thus ( M is without_repeated_line implies Segm M,(Seg (len M)),((Seg (width M)) \ {i}) is without_repeated_line ) :: thesis: ( Segm M,(Seg (len M)),((Seg (width M)) \ {i}) is without_repeated_line implies M is without_repeated_line )

proof

assume A4: M is without_repeated_line ; :: thesis: Segm M,(Seg (len M)),((Seg (width M)) \ {i}) is without_repeated_line
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) or not x2 in dom (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) or not (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . x1 = (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . x2 or x1 = x2 )
assume A5: ( x1 in dom (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) & x2 in dom (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) & (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . x1 = (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . x2 ) ; :: thesis: x1 = x2
reconsider i1 = x1, i2 = x2 as Element of NAT by A5;
A6: ( (Seg (width M)) \ {i} c= Seg (width M) & Sgm (Seg (len M)) = idseq m ) by A2, FINSEQ_3:54, XBOOLE_1:36;
then A7: (Line M,i1) * (Sgm ((Seg (width M)) \ {i})) = (Line M,((Sgm (Seg (len M))) . i1)) * (Sgm ((Seg (width M)) \ {i})) by A3, A5, FINSEQ_2:57
.= Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),i1 by A2, A3, A5, A6, Th47
.= (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . i1 by A2, A3, A5, MATRIX_2:10
.= Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),i2 by A2, A3, A5, MATRIX_2:10
.= (Line M,((Sgm (Seg (len M))) . i2)) * (Sgm ((Seg (width M)) \ {i})) by A2, A3, A5, A6, Th47
.= (Line M,i2) * (Sgm ((Seg (width M)) \ {i})) by A3, A5, A6, FINSEQ_2:57 ;
A8: ( len (Line M,i1) = width M & len (Line M,i2) = width M ) by FINSEQ_1:def 18;

now

let k be Nat; :: thesis: ( 1 <= k & k <= width M implies (Line M,i1) . b₁ = (Line M,i2) . b₁ )
assume A9: ( 1 <= k & k <= width M ) ; :: thesis: (Line M,i1) . b₁ = (Line M,i2) . b₁
k in NAT by ORDINAL1:def 13;
then A10: k in Seg (width M) by A9;

per cases ( k = i or k <> i ) ;

suppose k = i ; :: thesis: (Line M,i1) . b₁ = (Line M,i2) . b₁

then ( M * i1,k = a & M * i2,k = a & M * i1,k = (Line M,i1) . k ) by A1, A3, A5, A10, MATRIX_1:def 8;
hence (Line M,i1) . k = (Line M,i2) . k by A10, MATRIX_1:def 8; :: thesis: verum

end;

suppose k <> i ; :: thesis: (Line M,i1) . b₁ = (Line M,i2) . b₁

then ( k in (Seg (width M)) \ {i} & rng (Sgm ((Seg (width M)) \ {i})) = (Seg (width M)) \ {i} ) by A6, A10, FINSEQ_1:def 13, ZFMISC_1:64;
then consider x being set such that
A11: ( x in dom (Sgm ((Seg (width M)) \ {i})) & (Sgm ((Seg (width M)) \ {i})) . x = k ) by FUNCT_1:def 5;
thus (Line M,i1) . k = ((Line M,i1) * (Sgm ((Seg (width M)) \ {i}))) . x by A11, FUNCT_1:23
.= (Line M,i2) . k by A7, A11, FUNCT_1:23 ; :: thesis: verum

end;

end;

end;

then Line M,i1 = Line M,i2 by A8, FINSEQ_1:18
.= M . i2 by A3, A5, MATRIX_2:10 ;
then M . i1 = M . i2 by A3, A5, MATRIX_2:10;
hence x1 = x2 by A3, A4, A5, FUNCT_1:def 8; :: thesis: verum

end;

thus ( Segm M,(Seg (len M)),((Seg (width M)) \ {i}) is without_repeated_line implies M is without_repeated_line ) :: thesis: verum

proof

assume A12: Segm M,(Seg (len M)),((Seg (width M)) \ {i}) is without_repeated_line ; :: thesis: M is without_repeated_line
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom M or not x2 in dom M or not M . x1 = M . x2 or x1 = x2 )
assume A13: ( x1 in dom M & x2 in dom M & M . x1 = M . x2 ) ; :: thesis: x1 = x2
reconsider i1 = x1, i2 = x2 as Element of NAT by A13;
A14: ( (Seg (width M)) \ {i} c= Seg (width M) & Sgm (Seg (len M)) = idseq m ) by A2, FINSEQ_3:54, XBOOLE_1:36;
A15: ( Line M,i1 = M . i1 & Line M,i2 = M . i2 ) by A3, A13, MATRIX_2:10;
(Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . x1 = Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),i1 by A2, A3, A13, MATRIX_2:10
.= (Line M,((Sgm (Seg (len M))) . i1)) * (Sgm ((Seg (width M)) \ {i})) by A2, A3, A13, A14, Th47
.= (Line M,i2) * (Sgm ((Seg (width M)) \ {i})) by A3, A13, A14, A15, FINSEQ_2:57
.= (Line M,((Sgm (Seg (len M))) . i2)) * (Sgm ((Seg (width M)) \ {i})) by A3, A13, A14, FINSEQ_2:57
.= Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),i2 by A2, A3, A13, A14, Th47
.= (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . x2 by A2, A3, A13, MATRIX_2:10 ;
hence x1 = x2 by A3, A12, A13, FUNCT_1:def 8; :: thesis: verum

end;