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;