let x be set ; :: thesis: 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}; :: thesis: ( 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: ( dom f = [:{x},{x}:] & dom (x,x .--> x) = {[x,x]} & [:{x},{x}:] = {[x,x]} ) by FUNCT_2:def 1, ZFMISC_1:35;

now

let y be set ; :: thesis: ( y in {[x,x]} implies f . y = (x,x .--> x) . y )
assume A2: y in {[x,x]} ; :: thesis: f . y = (x,x .--> x) . y
then reconsider b = y as Element of [:{x},{x}:] by ZFMISC_1:35;
thus f . y = f . b
.= x by TARSKI:def 1
.= (x,x .--> x) . y by A2, FUNCOP_1:13 ; :: thesis: verum

end;

hence f = x,x .--> x by A1, FUNCT_1:9; :: thesis: ( f is having_a_unity & f is commutative & f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )

A3: now

let a, b be Element of {x}; :: thesis: a = b
( a = x & b = x ) by TARSKI:def 1;
hence a = b ; :: thesis: verum

end;

then for b being Element of {x} holds
( f . a,b = b & f . b,a = b ) ;
then A4: a is_a_unity_wrt f by BINOP_1:11;
hence ex a being Element of {x} st a is_a_unity_wrt f ; :: according to SETWISEO:def 2 :: thesis: ( 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 A3; :: according to BINOP_1:def 13 :: thesis: ( 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 A3; :: according to BINOP_1:def 14 :: thesis: ( 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 A3; :: according to BINOP_1:def 15 :: thesis: ( 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 ) :: according to MONOID_0:def 5 :: thesis: ( f is cancelable & f is uniquely-decomposable )

proof

let a, b be Element of {x}; :: thesis: ex r, l being Element of {x} st
( f . a,r = b & f . l,a = b )
take a ; :: thesis: ex l being Element of {x} st
( f . a,a = b & f . l,a = b )
take a ; :: thesis: ( f . a,a = b & f . a,a = b )
thus ( f . a,a = b & f . a,a = b ) by A3; :: thesis: 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 A3; :: according to MONOID_0:def 8 :: thesis: f is uniquely-decomposable
thus ex a being Element of {x} st a is_a_unity_wrt f by A4; :: according to SETWISEO:def 2,MONOID_0:def 9 :: thesis: 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}; :: thesis: ( 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 A3; :: thesis: verum