let n, m, k, i be Nat; :: thesis: for K being Field
for a being Element of K
for A' being Matrix of m,n,K
for B' being Matrix of m,k,K st a <> 0. K holds
Solutions_of A',B' = Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
let K be Field; :: thesis: for a being Element of K
for A' being Matrix of m,n,K
for B' being Matrix of m,k,K st a <> 0. K holds
Solutions_of A',B' = Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
let a be Element of K; :: thesis: for A' being Matrix of m,n,K
for B' being Matrix of m,k,K st a <> 0. K holds
Solutions_of A',B' = Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
let A' be Matrix of m,n,K; :: thesis: for B' being Matrix of m,k,K st a <> 0. K holds
Solutions_of A',B' = Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
let B' be Matrix of m,k,K; :: thesis: ( a <> 0. K implies Solutions_of A',B' = Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i))) )
assume A1: a <> 0. K ; :: thesis: Solutions_of A',B' = Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
set RA = RLine A',i,(a * (Line A',i));
set RB = RLine B',i,(a * (Line B',i));
thus Solutions_of A',B' c= Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i))) :: according to XBOOLE_0:def 10 :: thesis: Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i))) 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,(a * (Line A',i))),(RLine B',i,(a * (Line B',i))) )
assume A2: x in Solutions_of A',B' ; :: thesis: x in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
ex X being Matrix of K st
( x = X & len X = width A' & width X = width B' & A' * X = B' ) by A2;
hence x in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i))) by A2, Th38; :: thesis: verum

end;

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

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

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

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

end;

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

consider X being Matrix of K such that
A6: ( x = X & len X = width (RLine A',i,(a * (Line A',i))) & width X = width (RLine B',i,(a * (Line B',i))) ) and
(RLine A',i,(a * (Line A',i))) * X = RLine B',i,(a * (Line B',i)) by A3;
set RRA = RLine (RLine A',i,(a * (Line A',i))),i,((a " ) * (Line (RLine A',i,(a * (Line A',i))),i));
set RRB = RLine (RLine B',i,(a * (Line B',i))),i,((a " ) * (Line (RLine B',i,(a * (Line B',i))),i));
A7: ( len (a * (Line A',i)) = width A' & len ((a " ) * (Line (RLine A',i,(a * (Line A',i))),i)) = width (RLine A',i,(a * (Line A',i))) & len (a * (Line B',i)) = width B' & len ((a " ) * (Line (RLine B',i,(a * (Line B',i))),i)) = width (RLine B',i,(a * (Line B',i))) ) by FINSEQ_1:def 18;
then A8: ( width (RLine A',i,(a * (Line A',i))) = width A' & width (RLine B',i,(a * (Line B',i))) = width B' ) by MATRIX11:def 3;
reconsider aLA = a * (Line A',i), aLB = a * (Line B',i), aLAR = (a " ) * (Line (RLine A',i,(a * (Line A',i))),i), aLBR = (a " ) * (Line (RLine B',i,(a * (Line B',i))),i) as Element of the carrier of K * by FINSEQ_1:def 11;
A9: (a " ) * (Line (RLine A',i,(a * (Line A',i))),i) = (a " ) * (a * (Line A',i)) by A5, A7, MATRIX11:28
.= ((a " ) * a) * (Line A',i) by FVSUM_1:67
.= (1_ K) * (Line A',i) by A1, VECTSP_1:def 22
.= Line A',i by FVSUM_1:70 ;
A10: (a " ) * (Line (RLine B',i,(a * (Line B',i))),i) = (a " ) * (a * (Line B',i)) by A5, A7, MATRIX11:28
.= ((a " ) * a) * (Line B',i) by FVSUM_1:67
.= (1_ K) * (Line B',i) by A1, VECTSP_1:def 22
.= Line B',i by FVSUM_1:70 ;
A11: RLine (RLine A',i,(a * (Line A',i))),i,((a " ) * (Line (RLine A',i,(a * (Line A',i))),i)) = Replace (RLine A',i,(a * (Line A',i))),i,aLAR by A7, MATRIX11:29
.= Replace (Replace A',i,aLA),i,aLAR by A7, MATRIX11:29
.= Replace A',i,aLAR by FUNCT_7:36
.= RLine A',i,(Line A',i) by A7, A8, A9, MATRIX11:29
.= A' by MATRIX11:30 ;
RLine (RLine B',i,(a * (Line B',i))),i,((a " ) * (Line (RLine B',i,(a * (Line B',i))),i)) = Replace (RLine B',i,(a * (Line B',i))),i,aLBR by A7, MATRIX11:29
.= Replace (Replace B',i,aLB),i,aLBR by A7, MATRIX11:29
.= Replace B',i,aLBR by FUNCT_7:36
.= RLine B',i,(Line B',i) by A7, A8, A10, MATRIX11:29
.= B' by MATRIX11:30 ;
hence x in Solutions_of A',B' by A6, A11, A3, Th38; :: thesis: verum

end;

end;