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

now :: thesis: for x being Element of F holds

( the addF of F . ((0. F),x) = x & the addF of F . (x,(0. F)) = x )

hence
0. F is_a_unity_wrt the addF of F
by BINOP_1:3; :: thesis: verum( the addF of F . ((0. F),x) = x & the addF of F . (x,(0. F)) = x )

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:2

.= x by RLVECT_1:4 ; :: thesis: the addF of F . (x,(0. F)) = x

thus the addF of F . (x,(0. F)) = x + (0. F)

.= x by RLVECT_1:4 ; :: thesis: verum

end;thus the addF of F . ((0. F),x) = x + (0. F) by RLVECT_1:2

.= x by RLVECT_1:4 ; :: thesis: the addF of F . (x,(0. F)) = x

thus the addF of F . (x,(0. F)) = x + (0. F)

.= x by RLVECT_1:4 ; :: thesis: verum