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

A17: now

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

now

per cases ;

suppose A26: o = i ; :: thesis:

then Line (RLine A',i,((Line A',i) + (a * (Line A',j)))),o = (Line A',i) + (a * (Line A',j)) by A7, A20, A24, MATRIX11:28;
hence ((RLine A',i,((Line A',i) + (a * (Line A',j)))) * X1) * o,p = ((Line A',i) + (a * (Line A',j))) "*" CX by A4, A9, A12, A13, A19, MATRIX_3:def 4
.= Sum ((mlt (Line A',i),CX) + (mlt (a * (Line A',j)),CX)) by A16, A22, MATRIX_4:56
.= Sum ((mlt (Line A',i),CX) + (a * (mlt (Line A',j),CX))) by FVSUM_1:82
.= (Sum (mlt (Line A',i),CX)) + (Sum (a * (mlt (Line A',j),CX))) by FVSUM_1:95
.= (B' * o,p) + (a * (B' * j,p)) by A21, A25, A26, FVSUM_1:92
.= LBop + (a * (B' * 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 B',i) + (a * (Line B',j))) . p by A23, A26, FVSUM_1:22
.= (RLine B',i,((Line B',i) + (a * (Line B',j)))) * o,p by A14, A13, A19, A26, MATRIX11:def 3 ;
:: thesis:

end;

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

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

end;

hence (RLine B',i,((Line B',i) + (a * (Line B',j)))) * o,p = ((RLine A',i,((Line A',i) + (a * (Line A',j)))) * X1) * o,p ; :: thesis:

end;

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