let i, j, k, m, n be Nat; :: thesis: for K being Field
for a being Element of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st j in Seg m & ( i = j implies a <> - (1_ K) ) holds
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)))))))

let K be Field; :: thesis: for a being Element of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st j in Seg m & ( i = j implies a <> - (1_ K) ) holds
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)))))))

let a be Element of K; :: thesis: for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st j in Seg m & ( i = j implies a <> - (1_ K) ) holds
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)))))))

let A9 be Matrix of m,n,K; :: thesis: for B9 being Matrix of m,k,K st j in Seg m & ( i = j implies a <> - (1_ K) ) holds
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)))))))

let B9 be Matrix of m,k,K; :: thesis: ( j in Seg m & ( i = j implies a <> - (1_ K) ) implies 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))))))) )
assume that
A1: j in Seg m and
A2: ( i = j implies a <> - (1_ K) ) ; :: thesis: 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)))))))
per cases ( i <> j or i = j ) ;
suppose i <> j ; :: thesis: 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)))))))
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 ; :: thesis: verum
end;
suppose A3: i = j ; :: thesis: 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)))))))
A4: (1_ K) + a <> 0. K
proof
assume (1_ K) + a = 0. K ; :: thesis: contradiction
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: verum
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: verum
end;
end;