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 6
.= (a + (b + c)) + d by RLVECT_1:def 6 ; :: thesis: verum