let m, n 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:
set V = n -VectSp_over K;
let i, j be Nat; :: thesis:
assume that
A3: j in Seg (len M) and
A4: i <> j ; :: thesis:
set Lj = Line (M,j);
set Li = Line (M,i);
set R = RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))));

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;

reconsider N = n as Element of NAT by ORDINAL1:def 12;
A6: dom M = Seg (len M) by FINSEQ_1:def 3;
then A7: M . i <> M . j by A2, A3, A4, A5;
A8: len M = m by MATRIX_0:def 2;
then A9: Line (M,j) in lines M by A3, Th103;
A10: Line (M,i) in lines M by A5, A8, Th103;
then reconsider LI = Line (M,i), LJ = Line (M,j) as Vector of (n -VectSp_over K) by A9;
reconsider li = LI, lj = LJ as Element of N -tuples_on the carrier of K by Th102;
A11: M . i = Line (M,i) by A5, A8, MATRIX_0:52;
m <> 0 by A5, A8;
then A12: n = width M by Th1;
A13: M . j = Line (M,j) by A3, A8, MATRIX_0:52;
A14: 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)))

a * lj = a * LJ by Th102;
then li + (a * lj) = LI + (a * LJ) by Th102
.= ((1_ K) * LI) + (a * LJ) by VECTSP_1:def 17 ;
then A15: li + (a * lj) in Lin {LI,LJ} by Th116;
let k be Nat; :: thesis:
assume that
A16: k in Seg m and
A17: k <> i ; :: thesis:
set Lk = Line (M,k);
assume A18: Line ((RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))),k) = (Line (M,i)) + (a * (Line (M,j))) ; :: thesis:
A19: Line ((RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))),k) = Line (M,k) by A16, A17, MATRIX11:28;
A20: Line (M,j) <> Line (M,k)

{LI,LJ} c= lines M by A10, A9, ZFMISC_1:32;
then A21: {LI,LJ} is linearly-independent by A1, VECTSP_7:1;
assume A22: Line (M,j) = Line (M,k) ; :: thesis:
A23: ((1_ K) + ((- (1_ K)) * a)) * LJ = ((1_ K) + ((- (1_ K)) * a)) * lj by Th102;
A24: (- (1_ K)) * LI = (- (1_ K)) * li by Th102;
0. (n -VectSp_over K) = n |-> (0. K) by Th102
.= lj + (- (li + (a * lj))) by A19, A18, A22, FVSUM_1:26
.= lj + ((- li) + (- (a * lj))) by FVSUM_1:31
.= lj + (((- (1_ K)) * li) + (- (a * lj))) by FVSUM_1:59
.= lj + (((- (1_ K)) * li) + ((- (1_ K)) * (a * lj))) by FVSUM_1:59
.= lj + (((- (1_ K)) * li) + (((- (1_ K)) * a) * lj)) by FVSUM_1:54
.= lj + ((((- (1_ K)) * a) * lj) + ((- (1_ K)) * li)) by FINSEQOP:33
.= (lj + (((- (1_ K)) * a) * lj)) + ((- (1_ K)) * li) by FINSEQOP:28
.= (((1_ K) * lj) + (((- (1_ K)) * a) * lj)) + ((- (1_ K)) * li) by FVSUM_1:57
.= (((1_ K) + ((- (1_ K)) * a)) * lj) + ((- (1_ K)) * li) by FVSUM_1:55
.= (((1_ K) + ((- (1_ K)) * a)) * LJ) + ((- (1_ K)) * LI) by A24, A23, Th102 ;
then - (1_ K) = 0. K by A7, A11, A13, A21, VECTSP_7:6;
hence contradiction by VECTSP_1:28; :: thesis:

end;

end;

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;
A29: len (li + (a * lj)) = n by CARD_1:def 7;
then RLine (M,i,(li + (a * lj))) = Replace (M,i,LiaLj) by A12, MATRIX11:29
.= M +* (i .--> LL) by A5, A6, FUNCT_7:def 3 ;
then A30: 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))
.= (M .: ((dom M) \ {i})) \/ {LL} by FUNCOP_1:8
.= ((M .: (dom M)) \ (M .: {i})) \/ {LL} by A2, FUNCT_1:64
.= ((lines M) \ (Im (M,i))) \/ {LL} by RELAT_1:113
.= ((lines M) \ {LI}) \/ {(li + (a * lj))} by A5, A6, A11, FUNCT_1:59 ;
A31: Line ((RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))),i) = (Line (M,i)) + (a * (Line (M,j))) by A5, A8, A29, A12, MATRIX11:28;

A32: len (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) = m by MATRIX_0:def 2;
let x1, x2 be object ; :: thesis:
assume that
A33: x1 in dom (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) and
A34: x2 in dom (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) and
A35: (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) . x1 = (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) . x2 ; :: thesis:
reconsider i1 = x1, i2 = x2 as Element of NAT by A33, A34;
A36: dom (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) = Seg (len (RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))))) by FINSEQ_1:def 3;
then A37: (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) . i1 = Line ((RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))),i1) by A33, A32, MATRIX_0:52;
A38: (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) . i2 = Line ((RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))),i2) by A34, A36, A32, MATRIX_0:52;

end;

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

end;

end;

end;