let n, m, l, k, i be Nat; :: thesis: for K being Field
for a being Element of K
for M, M1 being Matrix of n,m,K st l in dom M & k in dom M & i in dom M & M1 = RlineXScalar M,l,k,a holds
( ( i = l implies Line M1,i = (a * (Line M,k)) + (Line M,l) ) & ( i <> l implies Line M1,i = Line M,i ) )
let K be Field; :: thesis: for a being Element of K
for M, M1 being Matrix of n,m,K st l in dom M & k in dom M & i in dom M & M1 = RlineXScalar M,l,k,a holds
( ( i = l implies Line M1,i = (a * (Line M,k)) + (Line M,l) ) & ( i <> l implies Line M1,i = Line M,i ) )
let a be Element of K; :: thesis: for M, M1 being Matrix of n,m,K st l in dom M & k in dom M & i in dom M & M1 = RlineXScalar M,l,k,a holds
( ( i = l implies Line M1,i = (a * (Line M,k)) + (Line M,l) ) & ( i <> l implies Line M1,i = Line M,i ) )
let M, M1 be Matrix of n,m,K; :: thesis: ( l in dom M & k in dom M & i in dom M & M1 = RlineXScalar M,l,k,a implies ( ( i = l implies Line M1,i = (a * (Line M,k)) + (Line M,l) ) & ( i <> l 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 = RlineXScalar M,l,k,a ; :: thesis: ( ( i = l implies Line M1,i = (a * (Line M,k)) + (Line M,l) ) & ( i <> l implies Line M1,i = Line M,i ) )
thus ( i = l implies Line M1,i = (a * (Line M,k)) + (Line M,l) ) :: thesis: ( i <> l implies Line M1,i = Line M,i )

proof

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

now

let j be Nat; :: thesis: ( 1 <= j & j <= len (Line M1,i) implies (Line M1,i) . j = ((a * (Line M,k)) + (Line M,l)) . j )
assume A9: ( 1 <= j & j <= len (Line M1,i) ) ; :: thesis: (Line M1,i) . j = ((a * (Line M,k)) + (Line M,l)) . j
j in NAT by ORDINAL1:def 13;
then A10: j in Seg (width M1) by A6, A9;
then A11: (Line M,l) . j = M * l,j by A7, MATRIX_1:def 8;
then consider a2 being Element of K such that
A12: a2 = (Line M,l) . j ;
(a * (Line M,k)) . j = a * (M * k,j) by A2, A7, A10, Th3;
then consider a1 being Element of K such that
A13: a1 = (a * (Line M,k)) . j ;
j in dom ((a * (Line M,k)) + (Line M,l)) by A7, A5, A10, FINSEQ_1:def 3;
then A14: ((a * (Line M,k)) + (Line M,l)) . j = the addF of K . a1,a2 by A13, A12, FUNCOP_1:28
.= (a * (M * k,j)) + (M * l,j) by A2, A7, A10, A11, A13, A12, Th3 ;
thus (Line M1,i) . j = M1 * i,j by A10, MATRIX_1:def 8
.= ((a * (Line M,k)) + (Line M,l)) . j by A1, A2, A4, A8, A7, A10, A14, Def3 ; :: thesis: verum

end;

hence Line M1,i = (a * (Line M,k)) + (Line M,l) by A6, A5, Th1, FINSEQ_1:18; :: thesis: verum

end;

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

proof

A15: width M1 = width M by Th1;
A16: len (Line M1,i) = width M1 by MATRIX_1:def 8;
assume A17: i <> l ; :: thesis: Line M1,i = Line M,i

A18: now

let j be Nat; :: thesis: ( 1 <= j & j <= len (Line M1,i) implies (Line M1,i) . j = (Line M,i) . j )
assume A19: ( 1 <= j & j <= len (Line M1,i) ) ; :: thesis: (Line M1,i) . j = (Line M,i) . j
j in NAT by ORDINAL1:def 13;
then A20: j in Seg (width M1) by A16, A19;
hence (Line M1,i) . j = M1 * i,j by MATRIX_1:def 8
.= M * i,j by A2, A3, A4, A17, A15, A20, Def3
.= (Line M,i) . j by A15, A20, 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 A16, A18, Th1, FINSEQ_1:18; :: thesis: verum

end;