let n, m, k, 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 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 set ; :: 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;

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

suppose A4: 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,(a * (Line A9,i)) = A9 ) by A4, MATRIX13:40, MATRIX_1:def 3;
hence x in Solutions_of A9,B9 by A3, A4, MATRIX13:40; :: thesis: verum

end;

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 FINSEQ_1:def 18;
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:67
.= (1_ K) * (Line A9,i) by A1, VECTSP_1:def 22
.= Line A9,i by FVSUM_1:70 ;
A9: len (a * (Line B9,i)) = width B9 by FINSEQ_1:def 18;
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:67
.= (1_ K) * (Line B9,i) by A1, VECTSP_1:def 22
.= Line B9,i by FVSUM_1:70 ;
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 FINSEQ_1:def 18;
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:36
.= 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 FINSEQ_1:def 18;
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:36
.= 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;

end;