let F be Field; :: thesis: 0. F is_a_unity_wrt the addF of F

now

let x be Element of F; :: thesis: ( the addF of F . (0. F),x = x & the addF of F . x,(0. F) = x )
thus the addF of F . (0. F),x = x + (0. F) by RLVECT_1:5
.= x by RLVECT_1:10 ; :: thesis: the addF of F . x,(0. F) = x
thus the addF of F . x,(0. F) = x + (0. F)
.= x by RLVECT_1:10 ; :: thesis: verum

end;

hence 0. F is_a_unity_wrt the addF of F by BINOP_1:11; :: thesis: verum