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 11
.= (- (L + S)) + (- (- N)) by RLVECT_1:31
.= (- (L + S)) + N by RLVECT_1:17
.= ((- L) + (- S)) + N by RLVECT_1:31 ;
then K - R = ((L + M) - N) + (((- L) + (- S)) + N) by A1, RLVECT_1:def 11
.= ((M + L) + (- N)) + (((- L) + (- S)) + N) by RLVECT_1:def 11
.= ((M + L) + (- N)) + ((- S) + ((- L) + N)) by RLVECT_1:def 3
.= (M + (L + (- N))) + ((- S) + ((- L) + N)) by RLVECT_1:def 3
.= (M + (L - N)) + ((- S) + ((- L) + N)) by RLVECT_1:def 11
.= (M + (L - N)) + ((- S) + ((- L) + (- (- N)))) by RLVECT_1:17
.= (M + (L - N)) + ((- S) + (- (L + (- N)))) by RLVECT_1:31
.= (M + (L - N)) + ((- (L - N)) + (- S)) by RLVECT_1:def 11
.= ((M + (L - N)) + (- (L - N))) + (- S) by RLVECT_1:def 3
.= (M + ((L - N) + (- (L - N)))) + (- S) by RLVECT_1:def 3
.= (M + (0. F)) + (- S) by RLVECT_1:5
.= M + (- S) by RLVECT_1:4
.= (M * (1_ F)) + (- S)
.= (M * (1_ F)) + ((- S) * (1_ F))
.= (M + (- S)) * (1_ F)
.= (M - S) * (1_ F) by RLVECT_1:def 11 ;
hence (1_ F) * (M - S) = K - R ; :: thesis: verum