let m, n be Nat; :: thesis: for K being Field
for a being Element of K
for A' being Matrix of m,n,K
for i, j being Nat st j in Seg m & n > 0 & ( i = j implies a <> - (1_ K) ) holds
Space_of_Solutions_of A' = Space_of_Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j))))
let K be Field; :: thesis: for a being Element of K
for A' being Matrix of m,n,K
for i, j being Nat st j in Seg m & n > 0 & ( i = j implies a <> - (1_ K) ) holds
Space_of_Solutions_of A' = Space_of_Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j))))
let a be Element of K; :: thesis: for A' being Matrix of m,n,K
for i, j being Nat st j in Seg m & n > 0 & ( i = j implies a <> - (1_ K) ) holds
Space_of_Solutions_of A' = Space_of_Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j))))
let A' be Matrix of m,n,K; :: thesis: for i, j being Nat st j in Seg m & n > 0 & ( i = j implies a <> - (1_ K) ) holds
Space_of_Solutions_of A' = Space_of_Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j))))
let i, j be Nat; :: thesis: ( j in Seg m & n > 0 & ( i = j implies a <> - (1_ K) ) implies Space_of_Solutions_of A' = Space_of_Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))) )
assume that
A1: ( j in Seg m & n > 0 ) and
A2: ( i = j implies a <> - (1_ K) ) ; :: thesis: Space_of_Solutions_of A' = Space_of_Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j))))
set L = (len A') |-> (0. K);
( len ((len A') |-> (0. K)) = len A' & len A' = m ) by FINSEQ_1:def 18, MATRIX_1:def 3;
then reconsider C = ColVec2Mx ((len A') |-> (0. K)) as Matrix of m,1,K ;
set RC = RLine C,i,((Line C,i) + (a * (Line C,j)));
A3: ( C = 0. K,(len A'),1 & m <> 0 ) by Th32, A1;

now

let i', j' be Nat; :: thesis: ( [i',j'] in Indices C implies C * i',j' = (RLine C,i,((Line C,i) + (a * (Line C,j)))) * i',j' )
assume A4: [i',j'] in Indices C ; :: thesis: C * i',j' = (RLine C,i,((Line C,i) + (a * (Line C,j)))) * i',j'
reconsider I = i', J = j' as Element of NAT by ORDINAL1:def 13;
A5: len ((Line C,i) + (a * (Line C,j))) = width C by FINSEQ_1:def 18;

now

per cases ( i' = i or i <> i' ) ;

suppose A6: i' = i ; :: thesis: C * I,J = (RLine C,i,((Line C,i) + (a * (Line C,j)))) * I,J

m > 0 by A3;
then A7: ( len C = m & 1 = width C & Indices C = [:(Seg m),(Seg 1):] ) by MATRIX_1:24;
then A8: ( j' in Seg 1 & i' in Seg m ) by A4, ZFMISC_1:106;
then A9: ( (Line C,i) . j' = C * i,j' & (Line C,j) . j' = C * j,j' & [i,j'] in Indices C & [j,j'] in Indices C ) by A1, A7, A6, MATRIX_1:def 8, ZFMISC_1:106;
then (a * (Line C,j)) . j' = a * (C * j,j') by A7, A8, FVSUM_1:63;
then ((Line C,i) + (a * (Line C,j))) . j' = (C * i,j') + (a * (C * j,j')) by A7, A8, A9, FVSUM_1:22
.= (0. K) + (a * (C * j,j')) by A3, A9, MATRIX_3:3
.= (0. K) + (a * (0. K)) by A3, A9, MATRIX_3:3
.= (0. K) + (0. K) by VECTSP_1:36
.= 0. K by RLVECT_1:def 7
.= C * i',j' by A3, A4, MATRIX_3:3 ;
hence C * I,J = (RLine C,i,((Line C,i) + (a * (Line C,j)))) * I,J by A9, A6, A5, MATRIX11:def 3; :: thesis: verum

end;

suppose i <> i' ; :: thesis: C * I,J = (RLine C,i,((Line C,i) + (a * (Line C,j)))) * I,J

hence C * I,J = (RLine C,i,((Line C,i) + (a * (Line C,j)))) * I,J by A4, A5, MATRIX11:def 3; :: thesis: verum

end;

end;

end;

hence C * i',j' = (RLine C,i,((Line C,i) + (a * (Line C,j)))) * i',j' ; :: thesis: verum

end;

then A10: RLine C,i,((Line C,i) + (a * (Line C,j))) = C by MATRIX_1:28;
set R = RLine A',i,((Line A',i) + (a * (Line A',j)));
set SR = Space_of_Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j))));
set SA = Space_of_Solutions_of A';
m > 0 by A3;
then A11: ( len A' = m & len (RLine A',i,((Line A',i) + (a * (Line A',j)))) = m & width A' = n & width (RLine A',i,((Line A',i) + (a * (Line A',j)))) = n ) by MATRIX_1:24;
then ( Solutions_of A',C = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),C & the carrier of (Space_of_Solutions_of A') = Solutions_of A',((len A') |-> (0. K)) & the carrier of (Space_of_Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j))))) = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),((len A') |-> (0. K)) ) by A1, A2, A10, Th40, Def5;
hence Space_of_Solutions_of A' = Space_of_Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))) by A11, VECTSP_4:37; :: thesis: verum