let F be Field; :: thesis: for K, L, N, M being Element of F st K - L = N - M holds
M = (L + N) - K
let K, L, N, M be Element of F; :: thesis: ( K - L = N - M implies M = (L + N) - K )
assume K - L = N - M ; :: thesis: M = (L + N) - K
then M + (K + (- L)) = M + (N - M) by RLVECT_1:def 12;
then M + (K + (- L)) = M + (N + (- M)) by RLVECT_1:def 12;
then (M + K) + (- L) = M + (N + (- M)) by RLVECT_1:def 6;
then (M + K) + (- L) = (M + N) + (- M) by RLVECT_1:def 6;
then (M + K) - L = (N + M) + (- M) by RLVECT_1:def 12;
then (M + K) - L = N + (M + (- M)) by RLVECT_1:def 6;
then (M + K) - L = N + (0. F) by RLVECT_1:16;
then ((M + K) - L) + L = N + L by RLVECT_1:10;
then ((M + K) + (- L)) + L = N + L by RLVECT_1:def 12;
then (M + K) + ((- L) + L) = N + L by RLVECT_1:def 6;
then (M + K) + (0. F) = L + N by RLVECT_1:16;
then (M + K) + (- K) = (L + N) + (- K) by RLVECT_1:10;
then (M + K) + (- K) = (L + N) - K by RLVECT_1:def 12;
then M + (K + (- K)) = (L + N) - K by RLVECT_1:def 6;
then M + (0. F) = (L + N) - K by RLVECT_1:16;
hence M = (L + N) - K by RLVECT_1:10; :: thesis: verum