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)))))))

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 )
;

end;

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

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;proof

set LB = Line (B9,i);
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;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

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