let G be non empty multMagma ; :: thesis: ( G is unital iff ex a being Element of G st
for b being Element of G holds
( a * b = b & b * a = b ) )
thus ( G is unital implies ex a being Element of G st
for b being Element of G holds
( a * b = b & b * a = b ) ) :: thesis: ( ex a being Element of G st
for b being Element of G holds
( a * b = b & b * a = b ) implies G is unital )

proof

given a being Element of G such that A1: a is_a_unity_wrt the multF of G ; :: according to SETWISEO:def 2,MONOID_0:def 10 :: thesis: ex a being Element of G st
for b being Element of G holds
( a * b = b & b * a = b )
take a ; :: thesis: for b being Element of G holds
( a * b = b & b * a = b )
let b be Element of G; :: thesis: ( a * b = b & b * a = b )
( a is_a_left_unity_wrt H₂(G) & a is_a_right_unity_wrt the multF of G ) by A1, BINOP_1:def 7;
hence ( a * b = b & b * a = b ) by BINOP_1:def 5, BINOP_1:def 6; :: thesis: verum

end;

given a being Element of G such that A2: for b being Element of G holds
( a * b = b & b * a = b ) ; :: thesis: G is unital
take a ; :: 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