let F be Field; :: thesis: for K, N, M, L, 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, N, M, L, 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 14
.= (S + (- M)) + (0. F) by RLVECT_1:10
.= ((- M) + S) + ((- N) + N) by RLVECT_1:16
.= S + (((- N) + N) + (- M)) by RLVECT_1:def 6
.= S + ((- N) + (N + (- M))) by RLVECT_1:def 6
.= S + ((- N) + (N - M)) by RLVECT_1:def 14
.= (S + (- N)) + (N - M) by RLVECT_1:def 6
.= (S - N) + (N - M) by RLVECT_1:def 14 ;
then ((K * (N - M)) + (- (L * (N - S)))) + (L * (N - S)) = ((S - N) + (N - M)) + (L * (N - S)) by RLVECT_1:def 14;
then (K * (N - M)) + ((- (L * (N - S))) + (L * (N - S))) = ((S - N) + (N - M)) + (L * (N - S)) by RLVECT_1:def 6;
then (K * (N - M)) + (0. F) = ((S - N) + (N - M)) + (L * (N - S)) by RLVECT_1:16;
then K * (N - M) = ((S - N) + (N - M)) + (L * (N - S)) by RLVECT_1:10
.= ((S - N) + (L * (N - S))) + (N - M) by RLVECT_1:def 6 ;
then (K * (N - M)) + (- (N - M)) = ((S - N) + (L * (N - S))) + ((N - M) + (- (N - M))) by RLVECT_1:def 6
.= ((S - N) + (L * (N - S))) + (0. F) by RLVECT_1:16
.= (S - N) + (L * (N - S)) by RLVECT_1:10
.= (S + (- N)) + (L * (N - S)) by RLVECT_1:def 14
.= (L * (N - S)) + (- (N - S)) by RLVECT_1:47 ;
then (K * (N - M)) + (- ((1_ F) * (N - M))) = (L * (N - S)) + (- (N - S)) by VECTSP_1:def 19;
then (K * (N - M)) + ((- (1_ F)) * (N - M)) = (L * (N - S)) + (- (N - S)) by VECTSP_1:41;
then (K + (- (1_ F))) * (N - M) = (L * (N - S)) + (- (N - S)) by VECTSP_1:def 18
.= (L * (N - S)) + (- ((1_ F) * (N - S))) by VECTSP_1:def 19
.= (L * (N - S)) + ((- (1_ F)) * (N - S)) by VECTSP_1:41 ;
hence (K + (- (1_ F))) * (N - M) = (L + (- (1_ F))) * (N - S) by VECTSP_1:def 18; :: thesis: verum