let k, l, n, m, i be Nat; :: thesis: for K being comRing
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 comRing; :: 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 CARD_1:def 7;
A6: len (Line (M1,i)) = width M1 by MATRIX_0:def 7;
A7: width M1 = width M by Th1;
assume A8: i = l ; :: thesis: Line (M1,i) = (a * (Line (M,k))) + (Line (M,l))

now :: thesis: for j being Nat st 1 <= j & j <= len (Line (M1,i)) holds
(Line (M1,i)) . j = ((a * (Line (M,k))) + (Line (M,l))) . j

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
A10: j in Seg (width M1) by A6, A9;
then A11: (Line (M,l)) . j = M * (l,j) by A7, MATRIX_0:def 7;
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:22
.= (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_0:def 7
.= ((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; :: 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_0:def 7;
assume A17: i <> l ; :: thesis: Line (M1,i) = Line (M,i)

A18: now :: thesis: for j being Nat st 1 <= j & j <= len (Line (M1,i)) holds
(Line (M1,i)) . j = (Line (M,i)) . j

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
A20: j in Seg (width M1) by A16, A19;
hence (Line (M1,i)) . j = M1 * (i,j) by MATRIX_0:def 7
.= M * (i,j) by A2, A3, A4, A17, A15, A20, Def3
.= (Line (M,i)) . j by A15, A20, MATRIX_0:def 7 ;
:: thesis: verum

end;

len (Line (M,i)) = width M by MATRIX_0:def 7;
hence Line (M1,i) = Line (M,i) by A16, A18, Th1; :: thesis: verum

end;