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

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