let k, l, n, m be Nat; :: thesis:
let K be Field; :: thesis:
let M, M1 be Matrix of n,m,K; :: thesis:
let i be Nat; :: thesis:
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:
thus ( i = l implies Line (M1,i) = Line (M,k) ) :: thesis:

let j be Nat; :: thesis:
assume A9: ( 1 <= j & j <= len (Line (M1,i)) ) ; :: thesis:
A10: j in Seg (width M1) by A6, A9;
hence (Line (M1,i)) . j = M1 * (i,j) by MATRIX_0:def 7
.= M * (k,j) by A1, A4, A7, A5, A10, Def1
.= (Line (M,k)) . j by A5, A10, MATRIX_0:def 7 ;
:: thesis:

end;

len (Line (M,k)) = width M by MATRIX_0:def 7;
hence Line (M1,i) = Line (M,k) by A6, A8, Th1; :: thesis:

end;

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

let j be Nat; :: thesis:
assume A15: ( 1 <= j & j <= len (Line (M1,i)) ) ; :: thesis:
A16: j in Seg (width M1) by A12, A15;
hence (Line (M1,i)) . j = M1 * (i,j) by MATRIX_0:def 7
.= M * (l,j) by A2, A4, A13, A11, A16, Def1
.= (Line (M,l)) . j by A11, A16, MATRIX_0:def 7 ;
:: thesis:

end;

end;

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

let j be Nat; :: thesis:
assume A21: ( 1 <= j & j <= len (Line (M1,i)) ) ; :: thesis:
A22: j in Seg (width M1) by A18, A21;
hence (Line (M1,i)) . j = M1 * (i,j) by MATRIX_0:def 7
.= M * (i,j) by A3, A4, A19, A17, A22, Def1
.= (Line (M,i)) . j by A17, A22, MATRIX_0:def 7 ;
:: thesis:

end;

end;