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