let n, k, j, m, i be Nat; :: thesis: for K being Field
for a being Element of K
for A' being Matrix of m,n,K
for B' being Matrix of m,k,K st j in Seg m & ( i = j implies a <> - (1_ K) ) holds
Solutions_of A',B' = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),(RLine B',i,((Line B',i) + (a * (Line B',j))))
let K be Field; :: thesis: for a being Element of K
for A' being Matrix of m,n,K
for B' being Matrix of m,k,K st j in Seg m & ( i = j implies a <> - (1_ K) ) holds
Solutions_of A',B' = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),(RLine B',i,((Line B',i) + (a * (Line B',j))))
let a be Element of K; :: thesis: for A' being Matrix of m,n,K
for B' being Matrix of m,k,K st j in Seg m & ( i = j implies a <> - (1_ K) ) holds
Solutions_of A',B' = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),(RLine B',i,((Line B',i) + (a * (Line B',j))))
let A' be Matrix of m,n,K; :: thesis: for B' being Matrix of m,k,K st j in Seg m & ( i = j implies a <> - (1_ K) ) holds
Solutions_of A',B' = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),(RLine B',i,((Line B',i) + (a * (Line B',j))))
let B' be Matrix of m,k,K; :: thesis: ( j in Seg m & ( i = j implies a <> - (1_ K) ) implies Solutions_of A',B' = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),(RLine B',i,((Line B',i) + (a * (Line B',j)))) )
assume A1: ( j in Seg m & ( i = j implies a <> - (1_ K) ) ) ; :: thesis: Solutions_of A',B' = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),(RLine B',i,((Line B',i) + (a * (Line B',j))))

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

suppose i <> j ; :: thesis: Solutions_of A',B' = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),(RLine B',i,((Line B',i) + (a * (Line B',j))))

hence Solutions_of A',B' = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),(RLine B',i,((Line B',i) + (a * (Line B',j)))) by A1, Lm5; :: thesis: verum

end;

suppose A2: i = j ; :: thesis: Solutions_of A',B' = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),(RLine B',i,((Line B',i) + (a * (Line B',j))))

set LA = Line A',i;
set LB = Line B',i;
A3: (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 A1, A2; :: thesis: verum

end;

A4: (Line A',i) + (a * (Line A',i)) = ((1_ K) * (Line A',i)) + (a * (Line A',i)) by FVSUM_1:70
.= ((1_ K) + a) * (Line A',i) by FVSUM_1:68 ;
(Line B',i) + (a * (Line B',i)) = ((1_ K) * (Line B',i)) + (a * (Line B',i)) by FVSUM_1:70
.= ((1_ K) + a) * (Line B',i) by FVSUM_1:68 ;
hence Solutions_of A',B' = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),(RLine B',i,((Line B',i) + (a * (Line B',j)))) by A2, A3, A4, Lm4; :: thesis: verum

end;

end;