let n, k, j, m, i be Nat; :: thesis:
let K be Field; :: thesis:
let a be Element of K; :: thesis:
let X be Matrix of K; :: thesis:
let A9 be Matrix of m,n,K; :: thesis:
let B9 be Matrix of m,k,K; :: thesis:
assume that
A1: X in Solutions_of A9,B9 and
A2: j in Seg m ; :: thesis:
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 FINSEQ_1:def 18;
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_1:27;
A14: len ((Line B9,i) + (a * (Line B9,j))) = width B9 by FINSEQ_1:def 18;
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 FINSEQ_1:def 18;

A17: now

A18: rng (a * (Line B9,j)) c= the carrier of K by FINSEQ_1:def 4;
let o, p be Nat; :: thesis:
assume A19: [o,p] in Indices (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))) ; :: thesis:
A20: o in dom B9 by A13, A19, ZFMISC_1:106;
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_1:def 9;
A23: p in Seg (width B9) by A13, A19, ZFMISC_1:106;
then ( B9 * o,p = (Line B9,o) . p & B9 * j,p = (Line B9,j) . p ) by MATRIX_1:def 8;
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:144;
then (a * (Line B9,j)) . p in rng (a * (Line B9,j)) by FUNCT_1:def 5;
then reconsider aLBjp = (a * (Line B9,j)) . p as Element of K by A18;
len B9 = m by MATRIX_1:def 3;
then A24: dom B9 = Seg m by FINSEQ_1:def 3;
then [j,p] in Indices B9 by A2, A23, ZFMISC_1:106;
then A25: B9 * j,p = (Line A9,j) "*" (Col X1,p) by A4, A6, MATRIX_3:def 4;

now

per cases ;

suppose A26: o = i ; :: thesis:

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:82
.= (Sum (mlt (Line A9,i),CX)) + (Sum (a * (mlt (Line A9,j),CX))) by FVSUM_1:95
.= (B9 * o,p) + (a * (B9 * j,p)) by A21, A25, A26, FVSUM_1:92
.= LBop + (a * (B9 * j,p)) by A23, MATRIX_1:def 8
.= LBop + (a * LBjp) by A23, MATRIX_1:def 8
.= LBop + aLBjp by A23, FVSUM_1:63
.= ((Line B9,i) + (a * (Line B9,j))) . p by A23, A26, FVSUM_1:22
.= (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))) * o,p by A14, A13, A19, A26, MATRIX11:def 3 ;
:: thesis:

end;

suppose A27: o <> i ; :: thesis:

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:

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:

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_1: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: