let F be Field; :: thesis: 1_ F is_a_unity_wrt the multF of F

now

let x be Element of F; :: thesis: ( the multF of F . (1_ F),x = x & the multF of F . x,(1_ F) = x )
thus the multF of F . (1_ F),x = (1_ F) * x
.= x by VECTSP_1:def 19 ; :: thesis: the multF of F . x,(1_ F) = x
thus the multF of F . x,(1_ F) = x * (1_ F)
.= x by VECTSP_1:def 19 ; :: thesis: verum

end;

hence 1_ F is_a_unity_wrt the multF of F by BINOP_1:11; :: thesis: verum