let G be non empty multMagma ; :: thesis: ( G is unital iff for a being Element of G holds
( (the_unity_wrt the multF of G) * a = a & a * (the_unity_wrt the multF of G) = a ) )
set u = the_unity_wrt the multF of G;
thus ( G is unital implies for b being Element of G holds
( (the_unity_wrt the multF of G) * b = b & b * (the_unity_wrt the multF of G) = b ) ) :: thesis: ( ( for a being Element of G holds
( (the_unity_wrt the multF of G) * a = a & a * (the_unity_wrt the multF of G) = a ) ) implies G is unital )

proof

given a being Element of G such that A1: a is_a_unity_wrt H₂(G) ; :: according to SETWISEO:def 2,MONOID_0:def 10 :: thesis: for b being Element of G holds
( (the_unity_wrt the multF of G) * b = b & b * (the_unity_wrt the multF of G) = b )
let b be Element of G; :: thesis: ( (the_unity_wrt the multF of G) * b = b & b * (the_unity_wrt the multF of G) = b )
the_unity_wrt the multF of G = a by A1, BINOP_1:def 8;
hence ( (the_unity_wrt the multF of G) * b = b & b * (the_unity_wrt the multF of G) = b ) by A1, BINOP_1:3; :: thesis: verum

end;

assume A2: for b being Element of G holds
( (the_unity_wrt the multF of G) * b = b & b * (the_unity_wrt the multF of G) = b ) ; :: thesis: G is unital
take a = the_unity_wrt the multF of G; :: according to SETWISEO:def 2,MONOID_0:def 10 :: thesis: a is_a_unity_wrt the multF of G
thus a is_a_left_unity_wrt the multF of G :: according to BINOP_1:def 7 :: thesis: a is_a_right_unity_wrt the multF of G

proof

let b be Element of G; :: according to BINOP_1:def 16 :: thesis: the multF of G . (a,b) = b
a * b = b by A2;
hence the multF of G . (a,b) = b ; :: thesis: verum

end;

let b be Element of G; :: according to BINOP_1:def 17 :: thesis: the multF of G . (b,a) = b
b * a = b by A2;
hence the multF of G . (b,a) = b ; :: thesis: verum