let F be Field; :: thesis: for K, L, M, N, R, S being Element of F st K = (L + M) - N & R = (L + S) - N holds
(1_ F) * (M - S) = K - R
let K, L, M, N, R, S be Element of F; :: thesis: ( K = (L + M) - N & R = (L + S) - N implies (1_ F) * (M - S) = K - R )
assume that
A1: K = (L + M) - N and
A2: R = (L + S) - N ; :: thesis: (1_ F) * (M - S) = K - R
- R = - ((L + S) + (- N)) by A2, RLVECT_1:def 14
.= (- (L + S)) + (- (- N)) by RLVECT_1:45
.= (- (L + S)) + N by RLVECT_1:30
.= ((- L) + (- S)) + N by RLVECT_1:45 ;
then K - R = ((L + M) - N) + (((- L) + (- S)) + N) by A1, RLVECT_1:def 14
.= ((M + L) + (- N)) + (((- L) + (- S)) + N) by RLVECT_1:def 14
.= ((M + L) + (- N)) + ((- S) + ((- L) + N)) by RLVECT_1:def 6
.= (M + (L + (- N))) + ((- S) + ((- L) + N)) by RLVECT_1:def 6
.= (M + (L - N)) + ((- S) + ((- L) + N)) by RLVECT_1:def 14
.= (M + (L - N)) + ((- S) + ((- L) + (- (- N)))) by RLVECT_1:30
.= (M + (L - N)) + ((- S) + (- (L + (- N)))) by RLVECT_1:45
.= (M + (L - N)) + ((- (L - N)) + (- S)) by RLVECT_1:def 14
.= ((M + (L - N)) + (- (L - N))) + (- S) by RLVECT_1:def 6
.= (M + ((L - N) + (- (L - N)))) + (- S) by RLVECT_1:def 6
.= (M + (0. F)) + (- S) by RLVECT_1:16
.= M + (- S) by RLVECT_1:10
.= (M * (1_ F)) + (- S) by VECTSP_1:def 19
.= (M * (1_ F)) + ((- S) * (1_ F)) by VECTSP_1:def 19
.= (M + (- S)) * (1_ F) by VECTSP_1:def 18
.= (M - S) * (1_ F) by RLVECT_1:def 14 ;
hence (1_ F) * (M - S) = K - R ; :: thesis: verum