let i, j, k, m, n be Nat; :: thesis: for K being Field
for a being Element of K
for X being Matrix of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds
X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))
let K be Field; :: thesis: for a being Element of K
for X being Matrix of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds
X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))
let a be Element of K; :: thesis: for X being Matrix of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds
X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))
let X be Matrix of K; :: thesis: for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds
X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))
let A9 be Matrix of m,n,K; :: thesis: for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds
X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))
let B9 be Matrix of m,k,K; :: thesis: ( X in Solutions_of (A9,B9) & j in Seg m implies X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j))))))) )
assume that
A1: X in Solutions_of (A9,B9) and
A2: j in Seg m ; :: thesis: X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))
consider X1 being Matrix of K such that
A3: X = X1 and
A4: len X1 = width A9 and
A5: width X1 = width B9 and
A6: A9 * X1 = B9 by A1;
set LAj = Line (A9,j);
set LAi = Line (A9,i);
set RA = RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))));
A7: len ((Line (A9,i)) + (a * (Line (A9,j)))) = width A9 by CARD_1:def 7;
then A8: len (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) = len A9 by MATRIX11:def 3;
set RX = (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1;
A9: width (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) = width A9 by A7, MATRIX11:def 3;
then A10: ( len ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) = len (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) & width ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) = width X1 ) by A4, MATRIX_3:def 4;
A11: len A9 = len B9 by A1, Th33;
then dom B9 = Seg (len (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))))) by A8, FINSEQ_1:def 3;
then A12: Indices ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) = Indices B9 by A5, A10, FINSEQ_1:def 3;
set LBj = Line (B9,j);
set LBi = Line (B9,i);
set RB = RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))));
A13: Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) = Indices B9 by MATRIX_0:26;
A14: len ((Line (B9,i)) + (a * (Line (B9,j)))) = width B9 by CARD_1:def 7;
then A15: width (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) = width B9 by MATRIX11:def 3;
A16: ( len (a * (Line (A9,j))) = width A9 & len (Line (A9,i)) = width A9 ) by CARD_1:def 7;

A17: now :: thesis: for o, p being Nat st [o,p] in Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) holds
(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p)

A18: rng (a * (Line (B9,j))) c= the carrier of K by FINSEQ_1:def 4;
let o, p be Nat; :: thesis: ( [o,p] in Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) implies (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) )
assume A19: [o,p] in Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) ; :: thesis: (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p)
A20: o in dom B9 by A13, A19, ZFMISC_1:87;
A21: B9 * (o,p) = (Line (A9,o)) "*" (Col (X1,p)) by A4, A6, A13, A19, MATRIX_3:def 4;
reconsider CX = Col (X1,p) as Element of (width A9) -tuples_on the carrier of K by A4;
A22: len (Col (X1,p)) = width A9 by A4, MATRIX_0:def 8;
A23: p in Seg (width B9) by A13, A19, ZFMISC_1:87;
then ( B9 * (o,p) = (Line (B9,o)) . p & B9 * (j,p) = (Line (B9,j)) . p ) by MATRIX_0:def 7;
then reconsider LBop = (Line (B9,o)) . p, LBjp = (Line (B9,j)) . p as Element of the carrier of K ;
p in dom (a * (Line (B9,j))) by A23, FINSEQ_2:124;
then (a * (Line (B9,j))) . p in rng (a * (Line (B9,j))) by FUNCT_1:def 3;
then reconsider aLBjp = (a * (Line (B9,j))) . p as Element of K by A18;
len B9 = m by MATRIX_0:def 2;
then A24: dom B9 = Seg m by FINSEQ_1:def 3;
then [j,p] in Indices B9 by A2, A23, ZFMISC_1:87;
then A25: B9 * (j,p) = (Line (A9,j)) "*" (Col (X1,p)) by A4, A6, MATRIX_3:def 4;

now :: thesis: ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p)

per cases ( o = i or o <> i ) ;

suppose A26: o = i ; :: thesis: ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p)

then Line ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),o) = (Line (A9,i)) + (a * (Line (A9,j))) by A7, A20, A24, MATRIX11:28;
hence ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = ((Line (A9,i)) + (a * (Line (A9,j)))) "*" CX by A4, A9, A12, A13, A19, MATRIX_3:def 4
.= Sum ((mlt ((Line (A9,i)),CX)) + (mlt ((a * (Line (A9,j))),CX))) by A16, A22, MATRIX_4:56
.= Sum ((mlt ((Line (A9,i)),CX)) + (a * (mlt ((Line (A9,j)),CX)))) by FVSUM_1:68
.= (Sum (mlt ((Line (A9,i)),CX))) + (Sum (a * (mlt ((Line (A9,j)),CX)))) by FVSUM_1:76
.= (B9 * (o,p)) + (a * (B9 * (j,p))) by A21, A25, A26, FVSUM_1:73
.= LBop + (a * (B9 * (j,p))) by A23, MATRIX_0:def 7
.= LBop + (a * LBjp) by A23, MATRIX_0:def 7
.= LBop + aLBjp by A23, FVSUM_1:51
.= ((Line (B9,i)) + (a * (Line (B9,j)))) . p by A23, A26, FVSUM_1:18
.= (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) by A14, A13, A19, A26, MATRIX11:def 3 ;
:: thesis: verum

end;

suppose A27: o <> i ; :: thesis: ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p)

then Line ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),o) = Line (A9,o) by A20, A24, MATRIX11:28;
hence ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = (Line (A9,o)) "*" (Col (X1,p)) by A4, A9, A12, A13, A19, MATRIX_3:def 4
.= B9 * (o,p) by A4, A6, A13, A19, MATRIX_3:def 4
.= (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) by A14, A13, A19, A27, MATRIX11:def 3 ;
:: thesis: verum

end;

end;

end;

hence (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) ; :: thesis: verum

end;

len (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) = len B9 by A14, MATRIX11:def 3;
then (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1 = RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j))))) by A5, A11, A8, A15, A10, A17, MATRIX_0:21;
hence X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j))))))) by A3, A4, A5, A9, A15; :: thesis: verum