let n, k, j, m, i 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 A1, Lm5; :: 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 7
.= ((- (1. K)) + (1_ K)) + a by RLVECT_1:def 6
.= (0. K) + a by VECTSP_1:66
.= a by RLVECT_1:def 7 ;
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:70
.= ((1_ K) + a) * (Line B9,i) by FVSUM_1:68 ;
(Line A9,i) + (a * (Line A9,i)) = ((1_ K) * (Line A9,i)) + (a * (Line A9,i)) by FVSUM_1:70
.= ((1_ K) + a) * (Line A9,i) by FVSUM_1:68 ;
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;