let m, n 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_0:def 2;
A3: card (Seg (len M)) = len M by FINSEQ_1:57;
len (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) = card (Seg (len M)) by MATRIX_0:def 2;
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

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 object ; :: according to FUNCT_1:def 4 :: 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 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:48;
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:49
.= 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_0:52
.= Line ((Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),i2) by A2, A3, A4, A9, A10, MATRIX_0:52
.= (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:49 ;

A13: now :: thesis: for k being Nat st 1 <= k & k <= width M holds
(Line (M,i1)) . k = (Line (M,i2)) . k

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₁
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_0:def 7;
M * (i1,k) = a by A1, A4, A8, A17;
hence (Line (M,i1)) . k = (Line (M,i2)) . k by A16, A18, A19, MATRIX_0:def 7; :: 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 FINSEQ_1:def 14;
k in (Seg (width M)) \ {i} by A16, A20, ZFMISC_1:56;
then consider x being object 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 3;
thus (Line (M,i1)) . k = ((Line (M,i1)) * (Sgm ((Seg (width M)) \ {i}))) . x by A22, A23, FUNCT_1:13
.= (Line (M,i2)) . k by A12, A22, A23, FUNCT_1:13 ; :: thesis: verum

end;

end;

end;

A24: len (Line (M,i2)) = width M by CARD_1:def 7;
len (Line (M,i1)) = width M by CARD_1:def 7;
then Line (M,i1) = Line (M,i2) by A24, A13
.= M . i2 by A4, A9, MATRIX_0:52 ;
then M . i1 = M . i2 by A4, A8, MATRIX_0:52;
hence x1 = x2 by A5, A4, A7, A8, A9; :: 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:48;
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 object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom M or not x2 in dom 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_0:52;
A31: Line (M,i2) = M . i2 by A5, A28, MATRIX_0:52;
(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_0:52
.= (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:49
.= (Line (M,((Sgm (Seg (len M))) . i2))) * (Sgm ((Seg (width M)) \ {i})) by A5, A28, A25, FINSEQ_2:49
.= 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_0:52 ;
hence x1 = x2 by A5, A4, A26, A27, A28; :: thesis: verum

end;