let F be Field; :: thesis: for L, K, 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 L, K, 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 12
.= R + (R + (- (K + N))) by RLVECT_1:47
.= R + (R + ((- K) + (- N))) by RLVECT_1:45
.= R + ((- N) + (R + (- K))) by RLVECT_1:def 6
.= (R + (- N)) + (R + (- K)) by RLVECT_1:def 6
.= (R - N) + (R + (- K)) by RLVECT_1:def 12
.= (R - K) + (R - N) by RLVECT_1:def 12 ;
(L * (R - N)) - (L * (R - K)) = (L * (R + (- N))) - (L * (R - K)) by RLVECT_1:def 12
.= (L * (R + (- N))) - (L * (R + (- K))) by RLVECT_1:def 12
.= (L * (R + (- N))) + (- (L * (R + (- K)))) by RLVECT_1:def 12
.= ((L * R) + (L * (- N))) + (- (L * (R + (- K)))) by VECTSP_1:def 18
.= ((L * R) + (L * (- N))) + ((- L) * (R + (- K))) by VECTSP_1:41
.= ((L * R) + (L * (- N))) + (((- L) * R) + ((- L) * (- K))) by VECTSP_1:def 18
.= ((L * R) + (L * (- N))) + (((- L) * R) + (L * K)) by VECTSP_1:42
.= ((L * (- N)) + (L * R)) + ((- (L * R)) + (L * K)) by VECTSP_1:41
.= (((L * (- N)) + (L * R)) + (- (L * R))) + (L * K) by RLVECT_1:def 6
.= ((L * (- N)) + ((L * R) + (- (L * R)))) + (L * K) by RLVECT_1:def 6
.= ((L * (- N)) + (0. F)) + (L * K) by RLVECT_1:16
.= (L * K) + (L * (- N)) by RLVECT_1:10
.= L * (K + (- N)) by VECTSP_1:def 18
.= L * (K - N) by RLVECT_1:def 12 ;
hence (L - (1_ F)) * (R - N) = (L + (1_ F)) * (R - K) by A1, Lm8; :: thesis: verum