let F be Field; :: thesis: for a, b, c, d being Element of F holds (a + b) + (c + d) = (a + (b + c)) + d
let a, b, c, d be Element of F; :: thesis: (a + b) + (c + d) = (a + (b + c)) + d
thus (a + b) + (c + d) = ((a + b) + c) + d by RLVECT_1:def 3
.= (a + (b + c)) + d by RLVECT_1:def 3 ; :: thesis: verum