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