let i, 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 a <> 0. K holds

Solutions_of (A9,B9) = 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 A9 being Matrix of m,n,K

for B9 being Matrix of m,k,K st a <> 0. K holds

Solutions_of (A9,B9) = Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i))))))

let a be Element of K; :: thesis: for A9 being Matrix of m,n,K

for B9 being Matrix of m,k,K st a <> 0. K holds

Solutions_of (A9,B9) = 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 a <> 0. K holds

Solutions_of (A9,B9) = 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: ( a <> 0. K implies Solutions_of (A9,B9) = Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i)))))) )

assume A1: a <> 0. K ; :: thesis: Solutions_of (A9,B9) = Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i))))))

set RB = RLine (B9,i,(a * (Line (B9,i))));

set RA = RLine (A9,i,(a * (Line (A9,i))));

thus Solutions_of (A9,B9) c= Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i)))))) :: according to XBOOLE_0:def 10 :: thesis: Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i)))))) c= Solutions_of (A9,B9)

assume A3: x in Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i)))))) ; :: 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 a <> 0. K holds

Solutions_of (A9,B9) = 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 A9 being Matrix of m,n,K

for B9 being Matrix of m,k,K st a <> 0. K holds

Solutions_of (A9,B9) = Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i))))))

let a be Element of K; :: thesis: for A9 being Matrix of m,n,K

for B9 being Matrix of m,k,K st a <> 0. K holds

Solutions_of (A9,B9) = 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 a <> 0. K holds

Solutions_of (A9,B9) = 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: ( a <> 0. K implies Solutions_of (A9,B9) = Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i)))))) )

assume A1: a <> 0. K ; :: thesis: Solutions_of (A9,B9) = Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i))))))

set RB = RLine (B9,i,(a * (Line (B9,i))));

set RA = RLine (A9,i,(a * (Line (A9,i))));

thus Solutions_of (A9,B9) c= Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i)))))) :: according to XBOOLE_0:def 10 :: thesis: Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i)))))) c= Solutions_of (A9,B9)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i)))))) 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,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i)))))) )

assume A2: 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))))))

ex X being Matrix of K st

( x = X & len X = width A9 & width X = width B9 & A9 * X = B9 ) by A2;

hence x in Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i)))))) by A2, Th38; :: thesis: verum

end;assume A2: 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))))))

ex X being Matrix of K st

( x = X & len X = width A9 & width X = width B9 & A9 * X = B9 ) by A2;

hence x in Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i)))))) by A2, Th38; :: thesis: verum

assume A3: x in Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i)))))) ; :: thesis: x in Solutions_of (A9,B9)

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

end;

suppose A4:
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,(a * (Line (A9,i)))) = A9 ) by A4, MATRIX13:40, MATRIX_0:def 2;

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

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

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

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

reconsider aLA = a * (Line (A9,i)), aLB = a * (Line (B9,i)), aLAR = (a ") * (Line ((RLine (A9,i,(a * (Line (A9,i))))),i)), aLBR = (a ") * (Line ((RLine (B9,i,(a * (Line (B9,i))))),i)) as Element of the carrier of K * by FINSEQ_1:def 11;

set RRB = RLine ((RLine (B9,i,(a * (Line (B9,i))))),i,((a ") * (Line ((RLine (B9,i,(a * (Line (B9,i))))),i))));

set RRA = RLine ((RLine (A9,i,(a * (Line (A9,i))))),i,((a ") * (Line ((RLine (A9,i,(a * (Line (A9,i))))),i))));

A6: ex X being Matrix of K st

( x = X & len X = width (RLine (A9,i,(a * (Line (A9,i))))) & width X = width (RLine (B9,i,(a * (Line (B9,i))))) & (RLine (A9,i,(a * (Line (A9,i))))) * X = RLine (B9,i,(a * (Line (B9,i)))) ) by A3;

A7: len (a * (Line (A9,i))) = width A9 by CARD_1:def 7;

then A8: (a ") * (Line ((RLine (A9,i,(a * (Line (A9,i))))),i)) = (a ") * (a * (Line (A9,i))) by A5, MATRIX11:28

.= ((a ") * a) * (Line (A9,i)) by FVSUM_1:54

.= (1_ K) * (Line (A9,i)) by A1, VECTSP_1:def 10

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

A9: len (a * (Line (B9,i))) = width B9 by CARD_1:def 7;

then A10: (a ") * (Line ((RLine (B9,i,(a * (Line (B9,i))))),i)) = (a ") * (a * (Line (B9,i))) by A5, MATRIX11:28

.= ((a ") * a) * (Line (B9,i)) by FVSUM_1:54

.= (1_ K) * (Line (B9,i)) by A1, VECTSP_1:def 10

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

A11: width (RLine (B9,i,(a * (Line (B9,i))))) = width B9 by A9, MATRIX11:def 3;

A12: len ((a ") * (Line ((RLine (B9,i,(a * (Line (B9,i))))),i))) = width (RLine (B9,i,(a * (Line (B9,i))))) by CARD_1:def 7;

then A13: RLine ((RLine (B9,i,(a * (Line (B9,i))))),i,((a ") * (Line ((RLine (B9,i,(a * (Line (B9,i))))),i)))) = Replace ((RLine (B9,i,(a * (Line (B9,i))))),i,aLBR) by MATRIX11:29

.= Replace ((Replace (B9,i,aLB)),i,aLBR) by A9, MATRIX11:29

.= Replace (B9,i,aLBR) by FUNCT_7:34

.= RLine (B9,i,(Line (B9,i))) by A12, A11, A10, MATRIX11:29

.= B9 by MATRIX11:30 ;

A14: width (RLine (A9,i,(a * (Line (A9,i))))) = width A9 by A7, MATRIX11:def 3;

A15: len ((a ") * (Line ((RLine (A9,i,(a * (Line (A9,i))))),i))) = width (RLine (A9,i,(a * (Line (A9,i))))) by CARD_1:def 7;

then RLine ((RLine (A9,i,(a * (Line (A9,i))))),i,((a ") * (Line ((RLine (A9,i,(a * (Line (A9,i))))),i)))) = Replace ((RLine (A9,i,(a * (Line (A9,i))))),i,aLAR) by MATRIX11:29

.= Replace ((Replace (A9,i,aLA)),i,aLAR) by A7, MATRIX11:29

.= Replace (A9,i,aLAR) by FUNCT_7:34

.= RLine (A9,i,(Line (A9,i))) by A15, A14, A8, MATRIX11:29

.= A9 by MATRIX11:30 ;

hence x in Solutions_of (A9,B9) by A3, A6, A13, Th38; :: thesis: verum

end;set RRB = RLine ((RLine (B9,i,(a * (Line (B9,i))))),i,((a ") * (Line ((RLine (B9,i,(a * (Line (B9,i))))),i))));

set RRA = RLine ((RLine (A9,i,(a * (Line (A9,i))))),i,((a ") * (Line ((RLine (A9,i,(a * (Line (A9,i))))),i))));

A6: ex X being Matrix of K st

( x = X & len X = width (RLine (A9,i,(a * (Line (A9,i))))) & width X = width (RLine (B9,i,(a * (Line (B9,i))))) & (RLine (A9,i,(a * (Line (A9,i))))) * X = RLine (B9,i,(a * (Line (B9,i)))) ) by A3;

A7: len (a * (Line (A9,i))) = width A9 by CARD_1:def 7;

then A8: (a ") * (Line ((RLine (A9,i,(a * (Line (A9,i))))),i)) = (a ") * (a * (Line (A9,i))) by A5, MATRIX11:28

.= ((a ") * a) * (Line (A9,i)) by FVSUM_1:54

.= (1_ K) * (Line (A9,i)) by A1, VECTSP_1:def 10

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

A9: len (a * (Line (B9,i))) = width B9 by CARD_1:def 7;

then A10: (a ") * (Line ((RLine (B9,i,(a * (Line (B9,i))))),i)) = (a ") * (a * (Line (B9,i))) by A5, MATRIX11:28

.= ((a ") * a) * (Line (B9,i)) by FVSUM_1:54

.= (1_ K) * (Line (B9,i)) by A1, VECTSP_1:def 10

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

A11: width (RLine (B9,i,(a * (Line (B9,i))))) = width B9 by A9, MATRIX11:def 3;

A12: len ((a ") * (Line ((RLine (B9,i,(a * (Line (B9,i))))),i))) = width (RLine (B9,i,(a * (Line (B9,i))))) by CARD_1:def 7;

then A13: RLine ((RLine (B9,i,(a * (Line (B9,i))))),i,((a ") * (Line ((RLine (B9,i,(a * (Line (B9,i))))),i)))) = Replace ((RLine (B9,i,(a * (Line (B9,i))))),i,aLBR) by MATRIX11:29

.= Replace ((Replace (B9,i,aLB)),i,aLBR) by A9, MATRIX11:29

.= Replace (B9,i,aLBR) by FUNCT_7:34

.= RLine (B9,i,(Line (B9,i))) by A12, A11, A10, MATRIX11:29

.= B9 by MATRIX11:30 ;

A14: width (RLine (A9,i,(a * (Line (A9,i))))) = width A9 by A7, MATRIX11:def 3;

A15: len ((a ") * (Line ((RLine (A9,i,(a * (Line (A9,i))))),i))) = width (RLine (A9,i,(a * (Line (A9,i))))) by CARD_1:def 7;

then RLine ((RLine (A9,i,(a * (Line (A9,i))))),i,((a ") * (Line ((RLine (A9,i,(a * (Line (A9,i))))),i)))) = Replace ((RLine (A9,i,(a * (Line (A9,i))))),i,aLAR) by MATRIX11:29

.= Replace ((Replace (A9,i,aLA)),i,aLAR) by A7, MATRIX11:29

.= Replace (A9,i,aLAR) by FUNCT_7:34

.= RLine (A9,i,(Line (A9,i))) by A15, A14, A8, MATRIX11:29

.= A9 by MATRIX11:30 ;

hence x in Solutions_of (A9,B9) by A3, A6, A13, Th38; :: thesis: verum