let X be non empty set ; :: thesis: for F being BinOp of X st F is having_a_unity holds
for x being Element of X holds
( F . ((the_unity_wrt F),x) = x & F . (x,(the_unity_wrt F)) = x )
let F be BinOp of X; :: thesis: ( F is having_a_unity implies for x being Element of X holds
( F . ((the_unity_wrt F),x) = x & F . (x,(the_unity_wrt F)) = x ) )
assume F is having_a_unity ; :: thesis: for x being Element of X holds
( F . ((the_unity_wrt F),x) = x & F . (x,(the_unity_wrt F)) = x )
then A1: the_unity_wrt F is_a_unity_wrt F by Th11;
let x be Element of X; :: thesis: ( F . ((the_unity_wrt F),x) = x & F . (x,(the_unity_wrt F)) = x )
thus ( F . ((the_unity_wrt F),x) = x & F . (x,(the_unity_wrt F)) = x ) by A1, BINOP_1:3; :: thesis: verum