let x be set ; for f being BinOp of {x} holds
( f = (x,x) .--> x & f is having_a_unity & f is commutative & f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
let f be BinOp of {x}; ( f = (x,x) .--> x & f is having_a_unity & f is commutative & f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
reconsider a = x as Element of {x} by TARSKI:def 1;
A1:
[:{x},{x}:] = {[x,x]}
by ZFMISC_1:29;
( dom f = [:{x},{x}:] & dom ((x,x) .--> x) = {[x,x]} )
by FUNCT_2:def 1;
hence
f = (x,x) .--> x
by A1, A2, FUNCT_1:2; ( f is having_a_unity & f is commutative & f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
then
for b being Element of {x} holds
( f . (a,b) = b & f . (b,a) = b )
;
then A5:
a is_a_unity_wrt f
by BINOP_1:3;
hence
ex a being Element of {x} st a is_a_unity_wrt f
; SETWISEO:def 2 ( f is commutative & f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
thus
for a, b being Element of {x} holds f . (a,b) = f . (b,a)
by A4; BINOP_1:def 2 ( f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
thus
for a, b, c being Element of {x} holds f . (a,(f . (b,c))) = f . ((f . (a,b)),c)
by A4; BINOP_1:def 3 ( f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
thus
for a being Element of {x} holds f . (a,a) = a
by A4; BINOP_1:def 4 ( f is invertible & f is cancelable & f is uniquely-decomposable )
thus
for a, b being Element of {x} ex r, l being Element of {x} st
( f . (a,r) = b & f . (l,a) = b )
MONOID_0:def 5 ( f is cancelable & f is uniquely-decomposable )proof
let a,
b be
Element of
{x};
ex r, l being Element of {x} st
( f . (a,r) = b & f . (l,a) = b )
take
a
;
ex l being Element of {x} st
( f . (a,a) = b & f . (l,a) = b )
take
a
;
( f . (a,a) = b & f . (a,a) = b )
thus
(
f . (
a,
a)
= b &
f . (
a,
a)
= b )
by A4;
verum
end;
thus
for a, b, c being Element of {x} st ( f . (a,b) = f . (a,c) or f . (b,a) = f . (c,a) ) holds
b = c
by A4; MONOID_0:def 8 f is uniquely-decomposable
thus
ex a being Element of {x} st a is_a_unity_wrt f
by A5; SETWISEO:def 2,MONOID_0:def 9 for a, b being Element of {x} st f . (a,b) = the_unity_wrt f holds
( a = b & b = the_unity_wrt f )
let a, b be Element of {x}; ( f . (a,b) = the_unity_wrt f implies ( a = b & b = the_unity_wrt f ) )
thus
( f . (a,b) = the_unity_wrt f implies ( a = b & b = the_unity_wrt f ) )
by A4; verum