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