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