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

proof

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

end;

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

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

suppose A5: not i in Seg m ; :: thesis: x in Solutions_of A',B'

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

end;

suppose A6: i in Seg m ; :: thesis: x in Solutions_of A',B'

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

end;

end;