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

now

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

now

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

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

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

end;

suppose i <> i9 ; :: 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 A7, A8, MATRIX11:def 3; :: thesis: verum

end;

end;

end;

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

end;

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