let f be BinOp of {} ; :: thesis: ( f is empty & f is associative & f is commutative )
[:{} ,{} :] = {}
by ZFMISC_1:113;
then A2:
( f c= [:(dom f),(rng f):] & dom f = {} & rng f c= {} )
;
thus
f is empty
; :: thesis: ( f is associative & f is commutative )
hereby :: according to BINOP_1:def 3 :: thesis: f is commutative
let a,
b,
c be
Element of
{} ;
:: thesis: f . a,(f . b,c) = f . (f . a,b),cthus f . a,
(f . b,c) =
{}
by A2, FUNCT_1:def 4
.=
f . (f . a,b),
c
by A2, FUNCT_1:def 4
;
:: thesis: verum
end;
let a, b be Element of {} ; :: according to BINOP_1:def 2 :: thesis: f . a,b = f . b,a
thus f . a,b =
{}
by A2, FUNCT_1:def 4
.=
f . b,a
by A2, FUNCT_1:def 4
; :: thesis: verum