let i, j, k, m, n 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)

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)

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 object ; :: 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) )
let x be object ; :: 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;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

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 )
;

end;

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

len A9 = m
by MATRIX_0:def 2;

then ( len B9 = m & RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))) = A9 ) by A5, MATRIX13:40, MATRIX_0:def 2;

hence x in Solutions_of (A9,B9) by A4, A5, MATRIX13:40; :: thesis: verum

end;then ( len B9 = m & RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))) = A9 ) by A5, MATRIX13:40, MATRIX_0:def 2;

hence x in Solutions_of (A9,B9) by A4, A5, MATRIX13:40; :: thesis: verum

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 CARD_1:def 7;

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

.= ((Line (B9,i)) + (a * (Line (B9,j)))) + (((- (1_ K)) * a) * (Line (B9,j))) by VECTSP_1:9

.= ((Line (B9,i)) + (a * (Line (B9,j)))) + ((- (1_ K)) * (a * (Line (B9,j)))) by FVSUM_1:54

.= ((Line (B9,i)) + (a * (Line (B9,j)))) + (- (a * (Line (B9,j)))) by FVSUM_1:59

.= (Line (B9,i)) + ((a * (Line (B9,j))) + (- (a * (Line (B9,j))))) by FINSEQOP:28

.= (Line (B9,i)) + ((width B9) |-> (0. K)) by FVSUM_1:26

.= Line (B9,i) by FVSUM_1:21 ;

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 CARD_1:def 7;

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:34

.= 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 CARD_1:def 7;

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

.= ((Line (A9,i)) + (a * (Line (A9,j)))) + (((- (1_ K)) * a) * (Line (A9,j))) by VECTSP_1:9

.= ((Line (A9,i)) + (a * (Line (A9,j)))) + ((- (1_ K)) * (a * (Line (A9,j)))) by FVSUM_1:54

.= ((Line (A9,i)) + (a * (Line (A9,j)))) + (- (a * (Line (A9,j)))) by FVSUM_1:59

.= (Line (A9,i)) + ((a * (Line (A9,j))) + (- (a * (Line (A9,j))))) by FINSEQOP:28

.= (Line (A9,i)) + ((width A9) |-> (0. K)) by FVSUM_1:26

.= Line (A9,i) by FVSUM_1:21 ;

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 CARD_1:def 7;

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:34

.= 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;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 CARD_1:def 7;

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

.= ((Line (B9,i)) + (a * (Line (B9,j)))) + (((- (1_ K)) * a) * (Line (B9,j))) by VECTSP_1:9

.= ((Line (B9,i)) + (a * (Line (B9,j)))) + ((- (1_ K)) * (a * (Line (B9,j)))) by FVSUM_1:54

.= ((Line (B9,i)) + (a * (Line (B9,j)))) + (- (a * (Line (B9,j)))) by FVSUM_1:59

.= (Line (B9,i)) + ((a * (Line (B9,j))) + (- (a * (Line (B9,j))))) by FINSEQOP:28

.= (Line (B9,i)) + ((width B9) |-> (0. K)) by FVSUM_1:26

.= Line (B9,i) by FVSUM_1:21 ;

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 CARD_1:def 7;

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:34

.= 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 CARD_1:def 7;

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

.= ((Line (A9,i)) + (a * (Line (A9,j)))) + (((- (1_ K)) * a) * (Line (A9,j))) by VECTSP_1:9

.= ((Line (A9,i)) + (a * (Line (A9,j)))) + ((- (1_ K)) * (a * (Line (A9,j)))) by FVSUM_1:54

.= ((Line (A9,i)) + (a * (Line (A9,j)))) + (- (a * (Line (A9,j)))) by FVSUM_1:59

.= (Line (A9,i)) + ((a * (Line (A9,j))) + (- (a * (Line (A9,j))))) by FINSEQOP:28

.= (Line (A9,i)) + ((width A9) |-> (0. K)) by FVSUM_1:26

.= Line (A9,i) by FVSUM_1:21 ;

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 CARD_1:def 7;

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:34

.= 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