let m, n, l, k be Nat; :: thesis: for K being Field
for M, M1 being Matrix of n,m,K
for i being Nat st l in dom M & k in dom M & i in dom M & M1 = InterchangeLine M,l,k holds
( ( i = l implies Line M1,i = Line M,k ) & ( i = k implies Line M1,i = Line M,l ) & ( i <> l & i <> k implies Line M1,i = Line M,i ) )
let K be Field; :: thesis: for M, M1 being Matrix of n,m,K
for i being Nat st l in dom M & k in dom M & i in dom M & M1 = InterchangeLine M,l,k holds
( ( i = l implies Line M1,i = Line M,k ) & ( i = k implies Line M1,i = Line M,l ) & ( i <> l & i <> k implies Line M1,i = Line M,i ) )
let M, M1 be Matrix of n,m,K; :: thesis: for i being Nat st l in dom M & k in dom M & i in dom M & M1 = InterchangeLine M,l,k holds
( ( i = l implies Line M1,i = Line M,k ) & ( i = k implies Line M1,i = Line M,l ) & ( i <> l & i <> k implies Line M1,i = Line M,i ) )
let i be Nat; :: thesis: ( l in dom M & k in dom M & i in dom M & M1 = InterchangeLine M,l,k implies ( ( i = l implies Line M1,i = Line M,k ) & ( i = k implies Line M1,i = Line M,l ) & ( i <> l & i <> k implies Line M1,i = Line M,i ) ) )
assume that
A1: l in dom M and
A2: k in dom M and
A3: i in dom M and
A4: M1 = InterchangeLine M,l,k ; :: thesis: ( ( i = l implies Line M1,i = Line M,k ) & ( i = k implies Line M1,i = Line M,l ) & ( i <> l & i <> k implies Line M1,i = Line M,i ) )
thus ( i = l implies Line M1,i = Line M,k ) :: thesis: ( ( i = k implies Line M1,i = Line M,l ) & ( i <> l & i <> k implies Line M1,i = Line M,i ) )

proof

A5: width M1 = width M by Th1;
A6: len (Line M1,i) = width M1 by MATRIX_1:def 8;
assume A7: i = l ; :: thesis: Line M1,i = Line M,k

A8: now

let j be Nat; :: thesis: ( 1 <= j & j <= len (Line M1,i) implies (Line M1,i) . j = (Line M,k) . j )
assume A9: ( 1 <= j & j <= len (Line M1,i) ) ; :: thesis: (Line M1,i) . j = (Line M,k) . j
j in NAT by ORDINAL1:def 13;
then A10: j in Seg (width M1) by A6, A9;
hence (Line M1,i) . j = M1 * i,j by MATRIX_1:def 8
.= M * k,j by A1, A4, A7, A5, A10, Def1
.= (Line M,k) . j by A5, A10, MATRIX_1:def 8 ;
:: thesis: verum

end;

len (Line M,k) = width M by MATRIX_1:def 8;
hence Line M1,i = Line M,k by A6, A8, Th1, FINSEQ_1:18; :: thesis: verum

end;

thus ( i = k implies Line M1,i = Line M,l ) :: thesis: ( i <> l & i <> k implies Line M1,i = Line M,i )

proof

A11: width M1 = width M by Th1;
A12: len (Line M1,i) = width M1 by MATRIX_1:def 8;
assume A13: i = k ; :: thesis: Line M1,i = Line M,l

A14: now

let j be Nat; :: thesis: ( 1 <= j & j <= len (Line M1,i) implies (Line M1,i) . j = (Line M,l) . j )
assume A15: ( 1 <= j & j <= len (Line M1,i) ) ; :: thesis: (Line M1,i) . j = (Line M,l) . j
j in NAT by ORDINAL1:def 13;
then A16: j in Seg (width M1) by A12, A15;
hence (Line M1,i) . j = M1 * i,j by MATRIX_1:def 8
.= M * l,j by A2, A4, A13, A11, A16, Def1
.= (Line M,l) . j by A11, A16, MATRIX_1:def 8 ;
:: thesis: verum

end;

len (Line M,l) = width M by MATRIX_1:def 8;
hence Line M1,i = Line M,l by A12, A14, Th1, FINSEQ_1:18; :: thesis: verum

end;

thus ( i <> l & i <> k implies Line M1,i = Line M,i ) :: thesis: verum

proof

A17: width M1 = width M by Th1;
A18: len (Line M1,i) = width M1 by MATRIX_1:def 8;
assume A19: ( i <> l & i <> k ) ; :: thesis: Line M1,i = Line M,i

A20: now

let j be Nat; :: thesis: ( 1 <= j & j <= len (Line M1,i) implies (Line M1,i) . j = (Line M,i) . j )
assume A21: ( 1 <= j & j <= len (Line M1,i) ) ; :: thesis: (Line M1,i) . j = (Line M,i) . j
j in NAT by ORDINAL1:def 13;
then A22: j in Seg (width M1) by A18, A21;
hence (Line M1,i) . j = M1 * i,j by MATRIX_1:def 8
.= M * i,j by A3, A4, A19, A17, A22, Def1
.= (Line M,i) . j by A17, A22, MATRIX_1:def 8 ;
:: thesis: verum

end;

len (Line M,i) = width M by MATRIX_1:def 8;
hence Line M1,i = Line M,i by A18, A20, Th1, FINSEQ_1:18; :: thesis: verum

end;