let F be Field; :: thesis: for a, b, c being Element of F holds (osf F) . (a,((osf F) . (b,c))) = the addF of F . (((osf F) . (a,b)),c)
let a, b, c be Element of F; :: thesis: (osf F) . (a,((osf F) . (b,c))) = the addF of F . (((osf F) . (a,b)),c)
thus (osf F) . (a,((osf F) . (b,c))) = (osf F) . (a,( the addF of F . (b,((comp F) . c)))) by Def1
.= a + ((comp F) . (b + ((comp F) . c))) by Def1
.= a + ((comp F) . (b + (- c))) by VECTSP_1:def 13
.= a + (- (b + (- c))) by VECTSP_1:def 13
.= a + ((- b) + (- (- c))) by RLVECT_1:31
.= a + (((comp F) . b) + (- (- c))) by VECTSP_1:def 13
.= a + (((comp F) . b) + ((comp F) . (- c))) by VECTSP_1:def 13
.= a + (((comp F) . b) + ((comp F) . ((comp F) . c))) by VECTSP_1:def 13
.= a + (((comp F) . b) + c) by REALSET2:9
.= (a + ((comp F) . b)) + c by RLVECT_1:def 3
.= the addF of F . (((osf F) . (a,b)),c) by Def1 ; :: thesis: verum