let f be BinOp of {}; :: thesis: ( f is empty & f is associative & f is commutative )
thus f is empty ; :: thesis: ( f is associative & f is commutative )
A1: f c= [:(dom f),(rng f):] ;

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)),c)
thus f . (a,(f . (b,c))) = {} by A1, FUNCT_1:def 2
.= f . ((f . (a,b)),c) by A1, FUNCT_1:def 2 ; :: 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 A1, FUNCT_1:def 2
.= f . (b,a) by A1, FUNCT_1:def 2 ; :: thesis: verum