let f be BinOp of {}; ( f is empty & f is associative & f is commutative )
thus
f is empty
; ( f is associative & f is commutative )
A1:
f c= [:(dom f),(rng f):]
;
hereby BINOP_1:def 3 f is commutative
let a,
b,
c be
Element of
{} ;
f . (a,(f . (b,c))) = f . ((f . (a,b)),c)thus f . (
a,
(f . (b,c))) =
{}
by A1, FUNCT_1:def 2
.=
f . (
(f . (a,b)),
c)
by A1, FUNCT_1:def 2
;
verum
end;
let a, b be Element of {} ; BINOP_1:def 2 f . (a,b) = f . (b,a)
thus f . (a,b) =
{}
by A1, FUNCT_1:def 2
.=
f . (b,a)
by A1, FUNCT_1:def 2
; verum