let F be Field; :: thesis: for a, b, c, d being Element of F holds

( a - b = c - d iff a + d = b + c )

let a, b, c, d be Element of F; :: thesis: ( a - b = c - d iff a + d = b + c )

then (b + c) - d = a + (d - d) by RLVECT_1:def 3

.= a + (0. F) by RLVECT_1:5

.= a by RLVECT_1:4 ;

hence a - b = ((c - d) + b) - b by RLVECT_1:def 3

.= (c - d) + (b - b) by RLVECT_1:def 3

.= (c - d) + (0. F) by RLVECT_1:5

.= c - d by RLVECT_1:4 ;

:: thesis: verum

( a - b = c - d iff a + d = b + c )

let a, b, c, d be Element of F; :: thesis: ( a - b = c - d iff a + d = b + c )

hereby :: thesis: ( a + d = b + c implies a - b = c - d )

assume
a + d = b + c
; :: thesis: a - b = c - dassume
a - b = c - d
; :: thesis: a + d = b + c

then (c - d) + b = (a + (- b)) + b

.= a + (b - b) by RLVECT_1:def 3

.= a + (0. F) by RLVECT_1:5

.= a by RLVECT_1:4 ;

hence a + d = ((c + b) + (- d)) + d by RLVECT_1:def 3

.= (c + b) + (d - d) by RLVECT_1:def 3

.= (c + b) + (0. F) by RLVECT_1:5

.= b + c by RLVECT_1:4 ;

:: thesis: verum

end;then (c - d) + b = (a + (- b)) + b

.= a + (b - b) by RLVECT_1:def 3

.= a + (0. F) by RLVECT_1:5

.= a by RLVECT_1:4 ;

hence a + d = ((c + b) + (- d)) + d by RLVECT_1:def 3

.= (c + b) + (d - d) by RLVECT_1:def 3

.= (c + b) + (0. F) by RLVECT_1:5

.= b + c by RLVECT_1:4 ;

:: thesis: verum

then (b + c) - d = a + (d - d) by RLVECT_1:def 3

.= a + (0. F) by RLVECT_1:5

.= a by RLVECT_1:4 ;

hence a - b = ((c - d) + b) - b by RLVECT_1:def 3

.= (c - d) + (b - b) by RLVECT_1:def 3

.= (c - d) + (0. F) by RLVECT_1:5

.= c - d by RLVECT_1:4 ;

:: thesis: verum