let n, m, k, i 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 holds
X in Solutions_of (RLine A9,i,(a * (Line A9,i))),(RLine B9,i,(a * (Line B9,i)))
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 holds
X in Solutions_of (RLine A9,i,(a * (Line A9,i))),(RLine B9,i,(a * (Line B9,i)))
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 holds
X in Solutions_of (RLine A9,i,(a * (Line A9,i))),(RLine B9,i,(a * (Line B9,i)))
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 holds
X in Solutions_of (RLine A9,i,(a * (Line A9,i))),(RLine B9,i,(a * (Line B9,i)))
let A9 be Matrix of m,n,K; :: thesis: for B9 being Matrix of m,k,K st X in Solutions_of A9,B9 holds
X in Solutions_of (RLine A9,i,(a * (Line A9,i))),(RLine B9,i,(a * (Line B9,i)))
let B9 be Matrix of m,k,K; :: thesis: ( X in Solutions_of A9,B9 implies X in Solutions_of (RLine A9,i,(a * (Line A9,i))),(RLine B9,i,(a * (Line B9,i))) )
set LA = Line A9,i;
set LB = Line B9,i;
set RA = RLine A9,i,(a * (Line A9,i));
set RB = RLine B9,i,(a * (Line B9,i));
A1: Indices (RLine B9,i,(a * (Line B9,i))) = Indices B9 by MATRIX_1:27;
A2: ( len (a * (Line B9,i)) = len (Line B9,i) & len (Line B9,i) = width B9 ) by FINSEQ_1:def 18, MATRIXR1:16;
then A3: width (RLine B9,i,(a * (Line B9,i))) = width B9 by MATRIX11:def 3;
A4: ( len (a * (Line A9,i)) = len (Line A9,i) & len (Line A9,i) = width A9 ) by FINSEQ_1:def 18, MATRIXR1:16;
then A5: len (RLine A9,i,(a * (Line A9,i))) = len A9 by MATRIX11:def 3;
assume A6: X in Solutions_of A9,B9 ; :: thesis: X in Solutions_of (RLine A9,i,(a * (Line A9,i))),(RLine B9,i,(a * (Line B9,i)))
then consider X1 being Matrix of K such that
A7: X = X1 and
A8: len X1 = width A9 and
A9: width X1 = width B9 and
A10: A9 * X1 = B9 ;
set RX = (RLine A9,i,(a * (Line A9,i))) * X1;
A11: width (RLine A9,i,(a * (Line A9,i))) = width A9 by A4, MATRIX11:def 3;
then A12: ( len ((RLine A9,i,(a * (Line A9,i))) * X1) = len (RLine A9,i,(a * (Line A9,i))) & width ((RLine A9,i,(a * (Line A9,i))) * X1) = width X1 ) by A8, MATRIX_3:def 4;
A13: len A9 = len B9 by A6, Th33;
then dom B9 = Seg (len (RLine A9,i,(a * (Line A9,i)))) by A5, FINSEQ_1:def 3;
then A14: Indices ((RLine A9,i,(a * (Line A9,i))) * X1) = Indices B9 by A9, A12, FINSEQ_1:def 3;

A15: now

len B9 = m by MATRIX_1:def 3;
then A16: dom B9 = Seg m by FINSEQ_1:def 3;
let j, k be Nat; :: thesis: ( [j,k] in Indices (RLine B9,i,(a * (Line B9,i))) implies (RLine B9,i,(a * (Line B9,i))) * j,k = ((RLine A9,i,(a * (Line A9,i))) * X1) * j,k )
assume A17: [j,k] in Indices (RLine B9,i,(a * (Line B9,i))) ; :: thesis: (RLine B9,i,(a * (Line B9,i))) * j,k = ((RLine A9,i,(a * (Line A9,i))) * X1) * j,k
A18: j in dom B9 by A1, A17, ZFMISC_1:106;
A19: k in Seg (width B9) by A1, A17, ZFMISC_1:106;
then B9 * i,k = (Line B9,i) . k by MATRIX_1:def 8;
then reconsider LBk = (Line B9,i) . k as Element of K ;
A20: B9 * j,k = (Line A9,j) "*" (Col X1,k) by A8, A10, A1, A17, MATRIX_3:def 4;

now

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

suppose A21: j = i ; :: thesis: ((RLine A9,i,(a * (Line A9,i))) * X1) * j,k = (RLine B9,i,(a * (Line B9,i))) * j,k

then Line (RLine A9,i,(a * (Line A9,i))),i = a * (Line A9,i) by A4, A18, A16, MATRIX11:28;
hence ((RLine A9,i,(a * (Line A9,i))) * X1) * j,k = (a * (Line A9,i)) "*" (Col X1,k) by A8, A11, A14, A1, A17, A21, MATRIX_3:def 4
.= Sum (a * (mlt (Line A9,i),(Col X1,k))) by A8, FVSUM_1:82
.= a * (Sum (mlt (Line A9,i),(Col X1,k))) by FVSUM_1:92
.= a * LBk by A19, A20, A21, MATRIX_1:def 8
.= (a * (Line B9,i)) . k by A19, FVSUM_1:63
.= (RLine B9,i,(a * (Line B9,i))) * j,k by A2, A1, A17, A21, MATRIX11:def 3 ;
:: thesis: verum

end;

suppose A22: j <> i ; :: thesis: ((RLine A9,i,(a * (Line A9,i))) * X1) * j,k = (RLine B9,i,(a * (Line B9,i))) * j,k

then Line (RLine A9,i,(a * (Line A9,i))),j = Line A9,j by A18, A16, MATRIX11:28;
hence ((RLine A9,i,(a * (Line A9,i))) * X1) * j,k = (Line A9,j) "*" (Col X1,k) by A8, A11, A14, A1, A17, MATRIX_3:def 4
.= B9 * j,k by A8, A10, A1, A17, MATRIX_3:def 4
.= (RLine B9,i,(a * (Line B9,i))) * j,k by A2, A1, A17, A22, MATRIX11:def 3 ;
:: thesis: verum

end;

end;

end;

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

end;

len (RLine B9,i,(a * (Line B9,i))) = len B9 by A2, MATRIX11:def 3;
then (RLine A9,i,(a * (Line A9,i))) * X1 = RLine B9,i,(a * (Line B9,i)) by A9, A13, A5, A3, A12, A15, MATRIX_1:21;
hence X in Solutions_of (RLine A9,i,(a * (Line A9,i))),(RLine B9,i,(a * (Line B9,i))) by A7, A8, A9, A11, A3; :: thesis: verum