let n, k, j, m, i be Nat; :: thesis: for K being Field
for a being Element of
for A' being Matrix of the carrier of K,m,
for B' being Matrix of the carrier of K,m, 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
for A' being Matrix of the carrier of K,m,
for B' being Matrix of the carrier of K,m, 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 ; :: thesis: for A' being Matrix of the carrier of K,m,
for B' being Matrix of the carrier of K,m, 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 the carrier of K,m,; :: thesis: for B' being Matrix of the carrier of K,m, 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 the carrier of K,m,; :: 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 that
A1: j in Seg m and
A2: ( 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 A3: 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))))

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 B',i;
set LA = Line A',i;
A5: (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 ;
(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 ;
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 A3, A4, A5, Lm4; :: thesis: verum

end;

end;