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 A1: 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 )
let x be Element of X; :: thesis: ( F . (the_unity_wrt F),x = x & F . x,(the_unity_wrt F) = x )
the_unity_wrt F is_a_unity_wrt F by A1, Th22;
hence ( F . (the_unity_wrt F),x = x & F . x,(the_unity_wrt F) = x ) by BINOP_1:11; :: thesis: verum