let F be Field; :: thesis: for a, b, c being Element of the carrier 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 the carrier 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 25
.= a + (- (b + (- c))) by VECTSP_1:def 25
.= a + ((- b) + (- (- c))) by RLVECT_1:45
.= a + (((comp F) . b) + (- (- c))) by VECTSP_1:def 25
.= a + (((comp F) . b) + ((comp F) . (- c))) by VECTSP_1:def 25
.= a + (((comp F) . b) + ((comp F) . ((comp F) . c))) by VECTSP_1:def 25
.= a + (((comp F) . b) + c) by REALSET2:13
.= (a + ((comp F) . b)) + c by RLVECT_1:def 6
.= the addF of F . ((osf F) . a,b),c by Def1 ; :: thesis: verum