let n, m be Nat; :: thesis: for K being Field
for M being Matrix of n,m,K
for i, j being Nat
for a being Element of K st M is one-to-one & j in dom M & ( i = j implies a <> - (1_ K) ) holds
Lin (lines M) = Lin (lines (RLine M,i,((Line M,i) + (a * (Line M,j)))))
let K be Field; :: thesis: for M being Matrix of n,m,K
for i, j being Nat
for a being Element of K st M is one-to-one & j in dom M & ( i = j implies a <> - (1_ K) ) holds
Lin (lines M) = Lin (lines (RLine M,i,((Line M,i) + (a * (Line M,j)))))
let M be Matrix of n,m,K; :: thesis: for i, j being Nat
for a being Element of K st M is one-to-one & j in dom M & ( i = j implies a <> - (1_ K) ) holds
Lin (lines M) = Lin (lines (RLine M,i,((Line M,i) + (a * (Line M,j)))))
let i, j be Nat; :: thesis: for a being Element of K st M is one-to-one & j in dom M & ( i = j implies a <> - (1_ K) ) holds
Lin (lines M) = Lin (lines (RLine M,i,((Line M,i) + (a * (Line M,j)))))
let a be Element of K; :: thesis: ( M is one-to-one & j in dom M & ( i = j implies a <> - (1_ K) ) implies Lin (lines M) = Lin (lines (RLine M,i,((Line M,i) + (a * (Line M,j))))) )
assume that
A1: M is one-to-one and
A2: j in dom M and
A3: ( i = j implies a <> - (1_ K) ) ; :: thesis: Lin (lines M) = Lin (lines (RLine M,i,((Line M,i) + (a * (Line M,j)))))
A4: len M = n by MATRIX_1:def 3;
set L = (Line M,i) + (a * (Line M,j));
A5: dom M = Seg (len M) by FINSEQ_1:def 3;
set R = RLine M,i,((Line M,i) + (a * (Line M,j)));

per cases ( not i in dom M or i in dom M ) ;

suppose not i in dom M ; :: thesis: Lin (lines M) = Lin (lines (RLine M,i,((Line M,i) + (a * (Line M,j)))))

hence Lin (lines M) = Lin (lines (RLine M,i,((Line M,i) + (a * (Line M,j))))) by A5, MATRIX13:40; :: thesis: verum

end;

suppose A6: i in dom M ; :: thesis: Lin (lines M) = Lin (lines (RLine M,i,((Line M,i) + (a * (Line M,j)))))

then n <> 0 by A5, A4;
then A7: width M = m by MATRIX_1:24;
then reconsider Li = Line M,i, Lj = Line M,j as Vector of (m -VectSp_over K) by MATRIX13:102;
a * Lj = a * (Line M,j) by A7, MATRIX13:102;
then A8: (Line M,i) + (a * (Line M,j)) = Li + (a * Lj) by A7, MATRIX13:102;
A9: ( not Li = Lj or a <> - (1_ K) or Li = 0. (m -VectSp_over K) )

proof

assume A10: Li = Lj ; :: thesis: ( a <> - (1_ K) or Li = 0. (m -VectSp_over K) )
( Li = M . i & Lj = M . j ) by A2, A5, A4, A6, MATRIX_2:10;
hence ( a <> - (1_ K) or Li = 0. (m -VectSp_over K) ) by A1, A2, A3, A6, A10, FUNCT_1:def 8; :: thesis: verum

end;

reconsider L9 = (Line M,i) + (a * (Line M,j)) as Element of the carrier of K * by FINSEQ_1:def 11;
reconsider LL = L9 as set ;
set iL = {i} --> L9;
len ((Line M,i) + (a * (Line M,j))) = width M by FINSEQ_1:def 18;
then A11: RLine M,i,((Line M,i) + (a * (Line M,j))) = M +* i,LL by MATRIX11:29
.= M +* (i .--> LL) by A6, FUNCT_7:def 3
.= M +* ({i} --> L9) by FUNCOP_1:def 9 ;
M .: ((dom M) \ (dom ({i} --> L9))) = (M .: (dom M)) \ (M .: (dom ({i} --> L9))) by A1, FUNCT_1:123
.= (rng M) \ (M .: (dom ({i} --> L9))) by RELAT_1:146
.= (rng M) \ (Im M,i) by FUNCOP_1:19
.= (rng M) \ {(M . i)} by A6, FUNCT_1:117
.= (rng M) \ {(Line M,i)} by A5, A4, A6, MATRIX_2:10 ;
then A12: lines (RLine M,i,((Line M,i) + (a * (Line M,j)))) = ((lines M) \ {(Line M,i)}) \/ (rng ({i} --> L9)) by A11, FRECHET:12
.= ((lines M) \ {(Line M,i)}) \/ {((Line M,i) + (a * (Line M,j)))} by FUNCOP_1:14 ;
A13: Lj in lines M by A2, A5, A4, MATRIX13:103;
Li in lines M by A5, A4, A6, MATRIX13:103;
hence Lin (lines M) = Lin (lines (RLine M,i,((Line M,i) + (a * (Line M,j))))) by A8, A12, A13, A9, Th14; :: thesis: verum

end;

end;