let F be Field; :: thesis: for K, L, M, N, S being Element of F st (K * (N - M)) - (L * (N - S)) = S - M holds
(K + (- (1_ F))) * (N - M) = (L + (- (1_ F))) * (N - S)
let K, L, M, N, S be Element of F; :: thesis: ( (K * (N - M)) - (L * (N - S)) = S - M implies (K + (- (1_ F))) * (N - M) = (L + (- (1_ F))) * (N - S) )
assume (K * (N - M)) - (L * (N - S)) = S - M ; :: thesis: (K + (- (1_ F))) * (N - M) = (L + (- (1_ F))) * (N - S)
then (K * (N - M)) - (L * (N - S)) = S + (- M) by RLVECT_1:def 11
.= (S + (- M)) + (0. F) by RLVECT_1:4
.= ((- M) + S) + ((- N) + N) by RLVECT_1:5
.= S + (((- N) + N) + (- M)) by RLVECT_1:def 3
.= S + ((- N) + (N + (- M))) by RLVECT_1:def 3
.= S + ((- N) + (N - M)) by RLVECT_1:def 11
.= (S + (- N)) + (N - M) by RLVECT_1:def 3
.= (S - N) + (N - M) by RLVECT_1:def 11 ;
then ((K * (N - M)) + (- (L * (N - S)))) + (L * (N - S)) = ((S - N) + (N - M)) + (L * (N - S)) by RLVECT_1:def 11;
then (K * (N - M)) + ((- (L * (N - S))) + (L * (N - S))) = ((S - N) + (N - M)) + (L * (N - S)) by RLVECT_1:def 3;
then (K * (N - M)) + (0. F) = ((S - N) + (N - M)) + (L * (N - S)) by RLVECT_1:5;
then K * (N - M) = ((S - N) + (N - M)) + (L * (N - S)) by RLVECT_1:4
.= ((S - N) + (L * (N - S))) + (N - M) by RLVECT_1:def 3 ;
then (K * (N - M)) + (- (N - M)) = ((S - N) + (L * (N - S))) + ((N - M) + (- (N - M))) by RLVECT_1:def 3
.= ((S - N) + (L * (N - S))) + (0. F) by RLVECT_1:5
.= (S - N) + (L * (N - S)) by RLVECT_1:4
.= (S + (- N)) + (L * (N - S)) by RLVECT_1:def 11
.= (L * (N - S)) + (- (N - S)) by RLVECT_1:33 ;
then (K * (N - M)) + (- ((1_ F) * (N - M))) = (L * (N - S)) + (- (N - S)) ;
then (K * (N - M)) + ((- (1_ F)) * (N - M)) = (L * (N - S)) + (- (N - S)) by VECTSP_1:9;
then (K + (- (1_ F))) * (N - M) = (L * (N - S)) + (- (N - S)) by VECTSP_1:def 7
.= (L * (N - S)) + (- ((1_ F) * (N - S)))
.= (L * (N - S)) + ((- (1_ F)) * (N - S)) by VECTSP_1:9 ;
hence (K + (- (1_ F))) * (N - M) = (L + (- (1_ F))) * (N - S) by VECTSP_1:def 7; :: thesis: verum