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 25
.= a + (0. F) by RLVECT_1:25
.= a by REALSET2:6 ; :: thesis: verum