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

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 A7: [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;
A8: len ((Line C,i) + (a * (Line C,j))) = width C by FINSEQ_1:def 18;

now

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

suppose A9: i' = 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: j' in Seg 1 by A7, ZFMISC_1:106;
then (Line C,j) . j' = C * j,j' by A10, MATRIX_1:def 8;
then A12: (a * (Line C,j)) . j' = a * (C * j,j') by A10, A11, FVSUM_1:63;
Indices C = [:(Seg m),(Seg 1):] by A4, MATRIX_1:24;
then A13: [j,j'] in Indices C by A1, A11, ZFMISC_1:106;
(Line C,i) . j' = C * i,j' by A10, A11, MATRIX_1:def 8;
then ((Line C,i) + (a * (Line C,j))) . j' = (C * i,j') + (a * (C * j,j')) by A10, A11, A12, FVSUM_1:22
.= (0. K) + (a * (C * j,j')) 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 * i',j' 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 <> 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 A7, A8, 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 RLine C,i,((Line C,i) + (a * (Line C,j))) = C by MATRIX_1:28;
then A14: Solutions_of A',C = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),C by A1, A3, Th40;
set SR = Space_of_Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j))));
( len A' = m & len (RLine A',i,((Line A',i) + (a * (Line A',j)))) = m ) by A4, MATRIX_1:24;
then A15: 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 A2, A5, Def5;
set SA = Space_of_Solutions_of A';
A16: width A' = n by A4, MATRIX_1:24;
then the carrier of (Space_of_Solutions_of A') = Solutions_of A',((len A') |-> (0. K)) by A2, Def5;
hence Space_of_Solutions_of A' = Space_of_Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))) by A16, A5, A14, A15, VECTSP_4:37; :: thesis: verum