let F be Field; :: thesis: for K, L, M, N being Element of F st K - L = N - M holds
M = (L + N) - K
let K, L, M, N 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 11;
then M + (K + (- L)) = M + (N + (- M)) by RLVECT_1:def 11;
then (M + K) + (- L) = M + (N + (- M)) by RLVECT_1:def 3;
then (M + K) + (- L) = (M + N) + (- M) by RLVECT_1:def 3;
then (M + K) - L = (N + M) + (- M) by RLVECT_1:def 11;
then (M + K) - L = N + (M + (- M)) by RLVECT_1:def 3;
then (M + K) - L = N + (0. F) by RLVECT_1:5;
then ((M + K) - L) + L = N + L by RLVECT_1:4;
then ((M + K) + (- L)) + L = N + L by RLVECT_1:def 11;
then (M + K) + ((- L) + L) = N + L by RLVECT_1:def 3;
then (M + K) + (0. F) = L + N by RLVECT_1:5;
then (M + K) + (- K) = (L + N) + (- K) by RLVECT_1:4;
then (M + K) + (- K) = (L + N) - K by RLVECT_1:def 11;
then M + (K + (- K)) = (L + N) - K by RLVECT_1:def 3;
then M + (0. F) = (L + N) - K by RLVECT_1:5;
hence M = (L + N) - K by RLVECT_1:4; :: thesis: verum