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