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