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 25
.= (a - b) - c by RLVECT_1:41
.= the addF of F . (the addF of F . a,(- b)),((comp F) . c) by VECTSP_1:def 25
.= the addF of F . (the addF of F . a,((comp F) . b)),((comp F) . c) by VECTSP_1:def 25
.= the addF of F . ((osf F) . a,b),((comp F) . c) by Def1
.= (osf F) . ((osf F) . a,b),c by Def1 ; :: thesis: verum