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