let n, k, j, m, i be Nat; :: thesis: for K being Field
for a being Element of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st j in Seg m & i <> j holds
Solutions_of A9,B9 = Solutions_of (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),(RLine B9,i,((Line B9,i) + (a * (Line B9,j))))
let K be Field; :: thesis: for a being Element of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st j in Seg m & i <> j holds
Solutions_of A9,B9 = Solutions_of (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),(RLine B9,i,((Line B9,i) + (a * (Line B9,j))))
let a be Element of K; :: thesis: for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st j in Seg m & i <> j holds
Solutions_of A9,B9 = Solutions_of (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),(RLine B9,i,((Line B9,i) + (a * (Line B9,j))))
let A9 be Matrix of m,n,K; :: thesis: for B9 being Matrix of m,k,K st j in Seg m & i <> j holds
Solutions_of A9,B9 = Solutions_of (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),(RLine B9,i,((Line B9,i) + (a * (Line B9,j))))
let B9 be Matrix of m,k,K; :: thesis: ( j in Seg m & i <> j implies Solutions_of A9,B9 = Solutions_of (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),(RLine B9,i,((Line B9,i) + (a * (Line B9,j)))) )
assume that
A1: j in Seg m and
A2: i <> j ; :: thesis: Solutions_of A9,B9 = Solutions_of (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),(RLine B9,i,((Line B9,i) + (a * (Line B9,j))))
set LB = Line B9,j;
set LA = Line A9,j;
set RA = RLine A9,i,((Line A9,i) + (a * (Line A9,j)));
set RB = RLine B9,i,((Line B9,i) + (a * (Line B9,j)));
thus Solutions_of A9,B9 c= Solutions_of (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),(RLine B9,i,((Line B9,i) + (a * (Line B9,j)))) :: according to XBOOLE_0:def 10 :: thesis: Solutions_of (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),(RLine B9,i,((Line B9,i) + (a * (Line B9,j)))) c= Solutions_of A9,B9

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of A9,B9 or x in Solutions_of (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),(RLine B9,i,((Line B9,i) + (a * (Line B9,j)))) )
assume A3: x in Solutions_of A9,B9 ; :: thesis: x in Solutions_of (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),(RLine B9,i,((Line B9,i) + (a * (Line B9,j))))
ex X being Matrix of K st
( x = X & len X = width A9 & width X = width B9 & A9 * X = B9 ) by A3;
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 A1, A3, Th39; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),(RLine B9,i,((Line B9,i) + (a * (Line B9,j)))) or x in Solutions_of A9,B9 )
assume A4: x in Solutions_of (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),(RLine B9,i,((Line B9,i) + (a * (Line B9,j)))) ; :: thesis: x in Solutions_of A9,B9

per cases ( not i in Seg m or i in Seg m ) ;

suppose A5: not i in Seg m ; :: thesis: x in Solutions_of A9,B9

len A9 = m by MATRIX_1:def 3;
then ( len B9 = m & RLine A9,i,((Line A9,i) + (a * (Line A9,j))) = A9 ) by A5, MATRIX13:40, MATRIX_1:def 3;
hence x in Solutions_of A9,B9 by A4, A5, MATRIX13:40; :: thesis: verum

end;

suppose A6: i in Seg m ; :: thesis: x in Solutions_of A9,B9

reconsider LLA = (Line A9,i) + (a * (Line A9,j)), LLB = (Line B9,i) + (a * (Line B9,j)), LLRA = (Line (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),i) + ((- a) * (Line (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),j)), LLRB = (Line (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),i) + ((- a) * (Line (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),j)) as Element of the carrier of K * by FINSEQ_1:def 11;
set RRB = RLine (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),i,((Line (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),i) + ((- a) * (Line (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),j)));
set RRA = RLine (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),i,((Line (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),i) + ((- a) * (Line (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),j)));
A7: ex X being Matrix of K st
( x = X & len X = width (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))) & width X = width (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))) & (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))) * X = RLine B9,i,((Line B9,i) + (a * (Line B9,j))) ) by A4;
A8: Line (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),j = Line B9,j by A1, A2, MATRIX11:28;
A9: len ((Line B9,i) + (a * (Line B9,j))) = width B9 by FINSEQ_1:def 18;
then A10: width (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))) = width B9 by MATRIX11:def 3;
Line (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),i = (Line B9,i) + (a * (Line B9,j)) by A6, A9, MATRIX11:28;
then A11: (Line (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),i) + ((- a) * (Line (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),j)) = ((Line B9,i) + (a * (Line B9,j))) + ((- ((1_ K) * a)) * (Line B9,j)) by A8, VECTSP_1:def 19
.= ((Line B9,i) + (a * (Line B9,j))) + (((- (1_ K)) * a) * (Line B9,j)) by VECTSP_1:41
.= ((Line B9,i) + (a * (Line B9,j))) + ((- (1_ K)) * (a * (Line B9,j))) by FVSUM_1:67
.= ((Line B9,i) + (a * (Line B9,j))) + (- (a * (Line B9,j))) by FVSUM_1:72
.= (Line B9,i) + ((a * (Line B9,j)) + (- (a * (Line B9,j)))) by FINSEQOP:29
.= (Line B9,i) + ((width B9) |-> (0. K)) by FVSUM_1:35
.= Line B9,i by FVSUM_1:28 ;
A12: len ((Line (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),i) + ((- a) * (Line (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),j))) = width (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))) by FINSEQ_1:def 18;
then A13: RLine (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),i,((Line (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),i) + ((- a) * (Line (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),j))) = Replace (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),i,LLRB by MATRIX11:29
.= Replace (Replace B9,i,LLB),i,LLRB by A9, MATRIX11:29
.= Replace B9,i,LLRB by FUNCT_7:36
.= RLine B9,i,((Line (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),i) + ((- a) * (Line (RLine B9,i,((Line B9,i) + (a * (Line B9,j)))),j))) by A12, A10, MATRIX11:29
.= B9 by A11, MATRIX11:30 ;
A14: Line (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),j = Line A9,j by A1, A2, MATRIX11:28;
A15: len ((Line A9,i) + (a * (Line A9,j))) = width A9 by FINSEQ_1:def 18;
then A16: width (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))) = width A9 by MATRIX11:def 3;
Line (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),i = (Line A9,i) + (a * (Line A9,j)) by A6, A15, MATRIX11:28;
then A17: (Line (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),i) + ((- a) * (Line (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),j)) = ((Line A9,i) + (a * (Line A9,j))) + ((- ((1_ K) * a)) * (Line A9,j)) by A14, VECTSP_1:def 19
.= ((Line A9,i) + (a * (Line A9,j))) + (((- (1_ K)) * a) * (Line A9,j)) by VECTSP_1:41
.= ((Line A9,i) + (a * (Line A9,j))) + ((- (1_ K)) * (a * (Line A9,j))) by FVSUM_1:67
.= ((Line A9,i) + (a * (Line A9,j))) + (- (a * (Line A9,j))) by FVSUM_1:72
.= (Line A9,i) + ((a * (Line A9,j)) + (- (a * (Line A9,j)))) by FINSEQOP:29
.= (Line A9,i) + ((width A9) |-> (0. K)) by FVSUM_1:35
.= Line A9,i by FVSUM_1:28 ;
A18: len ((Line (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),i) + ((- a) * (Line (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),j))) = width (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))) by FINSEQ_1:def 18;
then RLine (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),i,((Line (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),i) + ((- a) * (Line (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),j))) = Replace (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),i,LLRA by MATRIX11:29
.= Replace (Replace A9,i,LLA),i,LLRA by A15, MATRIX11:29
.= Replace A9,i,LLRA by FUNCT_7:36
.= RLine A9,i,((Line (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),i) + ((- a) * (Line (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))),j))) by A18, A16, MATRIX11:29
.= A9 by A17, MATRIX11:30 ;
hence x in Solutions_of A9,B9 by A1, A4, A7, A13, Th39; :: thesis: verum

end;

end;