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 )

hence
1_ F is_a_unity_wrt the multF of F
by BINOP_1:3; :: thesis: verum( 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;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