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 ;
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 ;
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 ;
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 ;
A13: len A9 = len B9 by ;
then dom B9 = Seg (len (RLine (A9,i,(a * (Line (A9,i)))))) by ;
then A14: Indices ((RLine (A9,i,(a * (Line (A9,i))))) * X1) = Indices B9 by ;
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 ;
A19: k in Seg (width B9) by ;
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 ;
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 ;
hence ((RLine (A9,i,(a * (Line (A9,i))))) * X1) * (j,k) = (a * (Line (A9,i))) "*" (Col (X1,k)) by
.= Sum (a * (mlt ((Line (A9,i)),(Col (X1,k))))) by
.= a * (Sum (mlt ((Line (A9,i)),(Col (X1,k))))) by FVSUM_1:73
.= a * LBk by
.= (a * (Line (B9,i))) . k by
.= (RLine (B9,i,(a * (Line (B9,i))))) * (j,k) by ;
:: 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 ;
hence ((RLine (A9,i,(a * (Line (A9,i))))) * X1) * (j,k) = (Line (A9,j)) "*" (Col (X1,k)) by
.= B9 * (j,k) by
.= (RLine (B9,i,(a * (Line (B9,i))))) * (j,k) by ;
:: 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 ;
then (RLine (A9,i,(a * (Line (A9,i))))) * X1 = RLine (B9,i,(a * (Line (B9,i)))) by ;
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