let i, 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) 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_0:26;
A2: ( len (a * (Line (B9,i))) = len (Line (B9,i)) & len (Line (B9,i)) = width B9 ) by CARD_1:def 7, 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 CARD_1:def 7, 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 :: thesis: for j, k being Nat st [j,k] in Indices (RLine (B9,i,(a * (Line (B9,i))))) holds
(RLine (B9,i,(a * (Line (B9,i))))) * (j,k) = ((RLine (A9,i,(a * (Line (A9,i))))) * X1) * (j,k)

len B9 = m by MATRIX_0:def 2;
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:87;
A19: k in Seg (width B9) by A1, A17, ZFMISC_1:87;
then B9 * (i,k) = (Line (B9,i)) . k by MATRIX_0:def 7;
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 :: thesis: ((RLine (A9,i,(a * (Line (A9,i))))) * X1) * (j,k) = (RLine (B9,i,(a * (Line (B9,i))))) * (j,k)

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:68
.= a * (Sum (mlt ((Line (A9,i)),(Col (X1,k))))) by FVSUM_1:73
.= a * LBk by A19, A20, A21, MATRIX_0:def 7
.= (a * (Line (B9,i))) . k by A19, FVSUM_1:51
.= (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_0: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