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

now :: thesis: for x being Element of F holds
( the multF of F . ((1_ F),x) = x & the multF of F . (x,(1_ F)) = x )

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 ; :: thesis: the multF of F . (x,(1_ F)) = x
thus the multF of F . (x,(1_ F)) = x * (1_ F)
.= x ; :: thesis: verum

end;

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