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_0:23;

len ((len A9) |-> (0. K)) = len A9 by CARD_1:def 7;

then len ((len A9) |-> (0. K)) = m by MATRIX_0:def 2;

then reconsider C = ColVec2Mx ((len A9) |-> (0. K)) as Matrix of m,1,K ;

set RC = RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))));

A6: C = 0. (K,(len A9),1) by Th32;

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_0:23;

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_0:23;

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:29; :: thesis: verum

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_0:23;

len ((len A9) |-> (0. K)) = len A9 by CARD_1:def 7;

then len ((len A9) |-> (0. K)) = m by MATRIX_0:def 2;

then reconsider C = ColVec2Mx ((len A9) |-> (0. K)) as Matrix of m,1,K ;

set RC = RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))));

A6: C = 0. (K,(len A9),1) by Th32;

now :: thesis: for i9, j9 being Nat st [i9,j9] in Indices C holds

C * (i9,j9) = (RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))))) * (i9,j9)

then
RLine (C,i,((Line (C,i)) + (a * (Line (C,j))))) = C
by MATRIX_0:27;C * (i9,j9) = (RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))))) * (i9,j9)

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 12;

A8: len ((Line (C,i)) + (a * (Line (C,j)))) = width C by CARD_1:def 7;

end;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 12;

A8: len ((Line (C,i)) + (a * (Line (C,j)))) = width C by CARD_1:def 7;

now :: thesis: C * (I,J) = (RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))))) * (I,J)end;

hence
C * (i9,j9) = (RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))))) * (i9,j9)
; :: thesis: verumper cases
( i9 = i or i <> i9 )
;

end;

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_0:23;

then A11: j9 in Seg 1 by A7, ZFMISC_1:87;

then (Line (C,j)) . j9 = C * (j,j9) by A10, MATRIX_0:def 7;

then A12: (a * (Line (C,j))) . j9 = a * (C * (j,j9)) by A10, A11, FVSUM_1:51;

Indices C = [:(Seg m),(Seg 1):] by A4, MATRIX_0:23;

then A13: [j,j9] in Indices C by A1, A11, ZFMISC_1:87;

(Line (C,i)) . j9 = C * (i,j9) by A10, A11, MATRIX_0:def 7;

then ((Line (C,i)) + (a * (Line (C,j)))) . j9 = (C * (i,j9)) + (a * (C * (j,j9))) by A10, A11, A12, FVSUM_1:18

.= (0. K) + (a * (C * (j,j9))) by A6, A7, A9, MATRIX_3:1

.= (0. K) + (a * (0. K)) by A6, A13, MATRIX_3:1

.= (0. K) + (0. K)

.= 0. K by RLVECT_1:def 4

.= C * (i9,j9) by A6, A7, MATRIX_3:1 ;

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;then A11: j9 in Seg 1 by A7, ZFMISC_1:87;

then (Line (C,j)) . j9 = C * (j,j9) by A10, MATRIX_0:def 7;

then A12: (a * (Line (C,j))) . j9 = a * (C * (j,j9)) by A10, A11, FVSUM_1:51;

Indices C = [:(Seg m),(Seg 1):] by A4, MATRIX_0:23;

then A13: [j,j9] in Indices C by A1, A11, ZFMISC_1:87;

(Line (C,i)) . j9 = C * (i,j9) by A10, A11, MATRIX_0:def 7;

then ((Line (C,i)) + (a * (Line (C,j)))) . j9 = (C * (i,j9)) + (a * (C * (j,j9))) by A10, A11, A12, FVSUM_1:18

.= (0. K) + (a * (C * (j,j9))) by A6, A7, A9, MATRIX_3:1

.= (0. K) + (a * (0. K)) by A6, A13, MATRIX_3:1

.= (0. K) + (0. K)

.= 0. K by RLVECT_1:def 4

.= C * (i9,j9) by A6, A7, MATRIX_3:1 ;

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

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_0:23;

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_0:23;

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:29; :: thesis: verum