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 Sl = Sgm (Seg (len M));
set SMi = (Seg (width M)) \ {i};
set S = Segm M,(Seg (len M)),((Seg (width M)) \ {i});
set Si = Sgm ((Seg (width M)) \ {i});
A2: len M = m by MATRIX_1:def 3;
A3: card (Seg (len M)) = len M by FINSEQ_1:78;
len (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) = card (Seg (len M)) by MATRIX_1:def 3;
then A4: dom (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) = Seg m by A2, A3, FINSEQ_1:def 3;
A5: dom M = Seg m by A2, 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

A6: (Seg (width M)) \ {i} c= Seg (width M) by XBOOLE_1:36;
assume A7: 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 proj1 (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) or not x2 in proj1 (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 that
A8: x1 in dom (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) and
A9: x2 in dom (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) and
A10: (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 A8, A9;
A11: Sgm (Seg (len M)) = idseq m by A2, FINSEQ_3:54;
then A12: (Line M,i1) * (Sgm ((Seg (width M)) \ {i})) = (Line M,((Sgm (Seg (len M))) . i1)) * (Sgm ((Seg (width M)) \ {i})) by A4, A8, FINSEQ_2:57
.= Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),i1 by A2, A3, A4, A8, Th47, XBOOLE_1:36
.= (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . i1 by A2, A3, A4, A8, MATRIX_2:10
.= Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),i2 by A2, A3, A4, A9, A10, MATRIX_2:10
.= (Line M,((Sgm (Seg (len M))) . i2)) * (Sgm ((Seg (width M)) \ {i})) by A2, A3, A4, A9, Th47, XBOOLE_1:36
.= (Line M,i2) * (Sgm ((Seg (width M)) \ {i})) by A4, A9, A11, FINSEQ_2:57 ;

A13: now

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

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

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

then A18: M * i2,k = a by A1, A4, A9;
A19: M * i1,k = (Line M,i1) . k by A16, MATRIX_1:def 8;
M * i1,k = a by A1, A4, A8, A17;
hence (Line M,i1) . k = (Line M,i2) . k by A16, A18, A19, MATRIX_1:def 8; :: thesis: verum

end;

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

A21: rng (Sgm ((Seg (width M)) \ {i})) = (Seg (width M)) \ {i} by A6, FINSEQ_1:def 13;
k in (Seg (width M)) \ {i} by A16, A20, ZFMISC_1:64;
then consider x being set such that
A22: x in dom (Sgm ((Seg (width M)) \ {i})) and
A23: (Sgm ((Seg (width M)) \ {i})) . x = k by A21, FUNCT_1:def 5;
thus (Line M,i1) . k = ((Line M,i1) * (Sgm ((Seg (width M)) \ {i}))) . x by A22, A23, FUNCT_1:23
.= (Line M,i2) . k by A12, A22, A23, FUNCT_1:23 ; :: thesis: verum

end;

end;

end;

A24: len (Line M,i2) = width M by FINSEQ_1:def 18;
len (Line M,i1) = width M by FINSEQ_1:def 18;
then Line M,i1 = Line M,i2 by A24, A13, FINSEQ_1:18
.= M . i2 by A4, A9, MATRIX_2:10 ;
then M . i1 = M . i2 by A4, A8, MATRIX_2:10;
hence x1 = x2 by A5, A4, A7, A8, A9, 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

A25: Sgm (Seg (len M)) = idseq m by A2, FINSEQ_3:54;
assume A26: 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 proj1 M or not x2 in proj1 M or not M . x1 = M . x2 or x1 = x2 )
assume that
A27: x1 in dom M and
A28: x2 in dom M and
A29: M . x1 = M . x2 ; :: thesis: x1 = x2
reconsider i1 = x1, i2 = x2 as Element of NAT by A27, A28;
A30: Line M,i1 = M . i1 by A5, A27, MATRIX_2:10;
A31: Line M,i2 = M . i2 by A5, A28, 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, A5, A27, MATRIX_2:10
.= (Line M,((Sgm (Seg (len M))) . i1)) * (Sgm ((Seg (width M)) \ {i})) by A2, A3, A5, A27, Th47, XBOOLE_1:36
.= (Line M,i2) * (Sgm ((Seg (width M)) \ {i})) by A5, A27, A29, A25, A30, A31, FINSEQ_2:57
.= (Line M,((Sgm (Seg (len M))) . i2)) * (Sgm ((Seg (width M)) \ {i})) by A5, A28, A25, FINSEQ_2:57
.= Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),i2 by A2, A3, A5, A28, Th47, XBOOLE_1:36
.= (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . x2 by A2, A3, A5, A28, MATRIX_2:10 ;
hence x1 = x2 by A5, A4, A26, A27, A28, FUNCT_1:def 8; :: thesis: verum

end;