let n, m be Nat; :: thesis:
let K be Field; :: thesis:
let a be Element of K; :: thesis:
let M be Matrix of m,n,K; :: thesis:
assume that
A1: lines M is linearly-independent and
A2: M is without_repeated_line ; :: thesis:
let i, j be Nat; :: thesis:
assume A3: ( j in Seg (len M) & i <> j ) ; :: thesis:
set V = n -VectSp_over K;
set Li = Line M,i;
set Lj = Line M,j;
set R = RLine M,i,((Line M,i) + (a * (Line M,j)));

per cases ;

suppose not i in Seg (len M) ; :: thesis:

hence ( RLine M,i,((Line M,i) + (a * (Line M,j))) is without_repeated_line & lines (RLine M,i,((Line M,i) + (a * (Line M,j)))) is linearly-independent ) by A1, A2, Th40; :: thesis:

end;

suppose A4: i in Seg (len M) ; :: thesis:

A5: ( len M = m & dom M = Seg (len M) ) by FINSEQ_1:def 3, MATRIX_1:def 3;
then A6: ( M . i <> M . j & M . i = Line M,i & M . j = Line M,j & Line M,i in lines M & Line M,j in lines M ) by A2, A3, A4, Th103, FUNCT_1:def 8, MATRIX_2:10;
then reconsider LI = Line M,i, LJ = Line M,j as Vector of (n -VectSp_over K) ;
reconsider N = n as Element of NAT by ORDINAL1:def 13;
reconsider li = LI, lj = LJ as Element of N -tuples_on the carrier of K by Th102;
A7: ((lines M) \ {LI}) \/ {(LI + (a * LJ))} is linearly-independent by A1, A6, Th115;
A8: for k being Nat st k in Seg m & k <> i holds
Line (RLine M,i,((Line M,i) + (a * (Line M,j)))),k <> (Line M,i) + (a * (Line M,j))

proof

let k be Nat; :: thesis:
assume A9: ( k in Seg m & k <> i ) ; :: thesis:
A10: Line (RLine M,i,((Line M,i) + (a * (Line M,j)))),k = Line M,k by A9, MATRIX11:28;
assume A11: Line (RLine M,i,((Line M,i) + (a * (Line M,j)))),k = (Line M,i) + (a * (Line M,j)) ; :: thesis:
set Lk = Line M,k;
A12: Line M,j <> Line M,k

proof

assume A13: Line M,j = Line M,k ; :: thesis:
{LI,LJ} c= lines M by A6, ZFMISC_1:38;
then A14: ( {LI,LJ} is linearly-independent & (- (1_ K)) * LI = (- (1_ K)) * li & ((1_ K) + ((- (1_ K)) * a)) * LJ = ((1_ K) + ((- (1_ K)) * a)) * lj ) by A1, Th102, VECTSP_7:2;
0. (n -VectSp_over K) = n |-> (0. K) by Th102
.= lj + (- (li + (a * lj))) by A10, A11, A13, FVSUM_1:35
.= lj + ((- li) + (- (a * lj))) by FVSUM_1:40
.= lj + (((- (1_ K)) * li) + (- (a * lj))) by FVSUM_1:72
.= lj + (((- (1_ K)) * li) + ((- (1_ K)) * (a * lj))) by FVSUM_1:72
.= lj + (((- (1_ K)) * li) + (((- (1_ K)) * a) * lj)) by FVSUM_1:67
.= lj + ((((- (1_ K)) * a) * lj) + ((- (1_ K)) * li)) by FINSEQOP:34
.= (lj + (((- (1_ K)) * a) * lj)) + ((- (1_ K)) * li) by FINSEQOP:29
.= (((1_ K) * lj) + (((- (1_ K)) * a) * lj)) + ((- (1_ K)) * li) by FVSUM_1:70
.= (((1_ K) + ((- (1_ K)) * a)) * lj) + ((- (1_ K)) * li) by FVSUM_1:68
.= (((1_ K) + ((- (1_ K)) * a)) * LJ) + ((- (1_ K)) * LI) by A14, Th102 ;
then - (1_ K) = 0. K by A6, A14, VECTSP_7:9;
hence contradiction by VECTSP_1:86; :: thesis:

end;

A15: ( M . i <> M . k & M . k = Line M,k & Line M,k in lines M ) by A2, A4, A5, A9, Th103, FUNCT_1:def 8, MATRIX_2:10;
then reconsider LK = Line M,k as Vector of (n -VectSp_over K) ;
reconsider KIJ = {LK,LI,LJ} as Subset of (n -VectSp_over K) ;
a * lj = a * LJ by Th102;
then li + (a * lj) = LI + (a * LJ) by Th102
.= ((1_ K) * LI) + (a * LJ) by VECTSP_1:def 26 ;
then A16: li + (a * lj) in Lin {LI,LJ} by Th116;
KIJ c= lines M by A6, A15, JORDAN16:2;
then ( Line M,k in KIJ & KIJ is linearly-independent & KIJ \ {LK} = {LI,LJ} ) by A1, A6, A12, A15, ENUMSET1:136, ENUMSET1:def 1, VECTSP_7:2;
hence contradiction by A10, A11, A16, VECTSP_9:18; :: thesis:

end;

A17: ( len (li + (a * lj)) = n & n = width M ) by A4, A5, Th1, FINSEQ_1:4, FINSEQ_1:def 18;
then A18: Line (RLine M,i,((Line M,i) + (a * (Line M,j)))),i = (Line M,i) + (a * (Line M,j)) by A4, A5, MATRIX11:28;

now

let x1, x2 be set ; :: thesis:
assume A19: ( x1 in dom (RLine M,i,((Line M,i) + (a * (Line M,j)))) & x2 in dom (RLine M,i,((Line M,i) + (a * (Line M,j)))) & (RLine M,i,((Line M,i) + (a * (Line M,j)))) . x1 = (RLine M,i,((Line M,i) + (a * (Line M,j)))) . x2 ) ; :: thesis:
A20: ( dom (RLine M,i,((Line M,i) + (a * (Line M,j)))) = Seg (len (RLine M,i,((Line M,i) + (a * (Line M,j))))) & len (RLine M,i,((Line M,i) + (a * (Line M,j)))) = m ) by FINSEQ_1:def 3, MATRIX_1:def 3;
reconsider i1 = x1, i2 = x2 as Element of NAT by A19;
A21: ( (RLine M,i,((Line M,i) + (a * (Line M,j)))) . i1 = Line (RLine M,i,((Line M,i) + (a * (Line M,j)))),i1 & (RLine M,i,((Line M,i) + (a * (Line M,j)))) . i2 = Line (RLine M,i,((Line M,i) + (a * (Line M,j)))),i2 ) by A19, A20, MATRIX_2:10;

per cases ;

suppose ( i1 = i & i2 = i ) ; :: thesis:

hence x1 = x2 ; :: thesis:

end;

suppose ( ( i1 = i & i2 <> i ) or ( i1 <> i & i2 = i ) ) ; :: thesis:

hence x1 = x2 by A8, A18, A19, A20, A21; :: thesis:

end;

suppose ( i1 <> i & i2 <> i ) ; :: thesis:

then ( (RLine M,i,((Line M,i) + (a * (Line M,j)))) . i1 = Line M,i1 & Line M,i1 = M . i1 & (RLine M,i,((Line M,i) + (a * (Line M,j)))) . i2 = Line M,i2 & Line M,i2 = M . i2 ) by A19, A20, A21, MATRIX11:28, MATRIX_2:10;
hence x1 = x2 by A2, A5, A19, A20, FUNCT_1:def 8; :: thesis:

end;

hence RLine M,i,((Line M,i) + (a * (Line M,j))) is without_repeated_line by FUNCT_1:def 8; :: thesis:
reconsider LiaLj = li + (a * lj) as Element of the carrier of K * by FINSEQ_1:def 11;
reconsider LL = LiaLj as set ;
set iLL = i .--> LL;
A22: a * lj = a * LJ by Th102;
RLine M,i,(li + (a * lj)) = Replace M,i,LiaLj by A17, MATRIX11:29
.= M +* (i .--> LL) by A4, A5, FUNCT_7:def 3 ;
then lines (RLine M,i,((Line M,i) + (a * (Line M,j)))) = (M .: ((dom M) \ (dom (i .--> LL)))) \/ (rng (i .--> LL)) by FRECHET:12
.= (M .: ((dom M) \ {i})) \/ (rng (i .--> LL)) by FUNCOP_1:19
.= (M .: ((dom M) \ {i})) \/ {LL} by FUNCOP_1:14
.= ((M .: (dom M)) \ (M .: {i})) \/ {LL} by A2, FUNCT_1:123
.= ((lines M) \ (Im M,i)) \/ {LL} by RELAT_1:146
.= ((lines M) \ {LI}) \/ {(li + (a * lj))} by A4, A5, A6, FUNCT_1:117 ;
hence lines (RLine M,i,((Line M,i) + (a * (Line M,j)))) is linearly-independent by A7, A22, Th102; :: thesis:

end;