let i, j, k, m, n be Nat; :: thesis:
let K be Field; :: thesis:
let a be Element of K; :: thesis:
let A9 be Matrix of m,n,K; :: thesis:
let B9 be Matrix of m,k,K; :: thesis:
assume that
A1: j in Seg m and
A2: ( i = j implies a <> - (1_ K) ) ; :: thesis:

hence Solutions_of (A9,B9) = Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j))))))) by A1, Lm5; :: thesis:

end;

assume (1_ K) + a = 0. K ; :: thesis:
then - (1. K) = (- (1. K)) + ((1_ K) + a) by RLVECT_1:def 4
.= ((- (1. K)) + (1_ K)) + a by RLVECT_1:def 3
.= (0. K) + a by VECTSP_1:19
.= a by RLVECT_1:def 4 ;
hence contradiction by A2, A3; :: thesis:

end;

set LB = Line (B9,i);
set LA = Line (A9,i);
A5: (Line (B9,i)) + (a * (Line (B9,i))) = ((1_ K) * (Line (B9,i))) + (a * (Line (B9,i))) by FVSUM_1:57
.= ((1_ K) + a) * (Line (B9,i)) by FVSUM_1:55 ;
(Line (A9,i)) + (a * (Line (A9,i))) = ((1_ K) * (Line (A9,i))) + (a * (Line (A9,i))) by FVSUM_1:57
.= ((1_ K) + a) * (Line (A9,i)) by FVSUM_1:55 ;
hence Solutions_of (A9,B9) = Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j))))))) by A3, A4, A5, Lm4; :: thesis:

end;