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):] ;

thus f . (a,b) = {} by A1, FUNCT_1:def 2

.= f . (b,a) by A1, FUNCT_1:def 2 ; :: thesis: verum

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 be Element of {} ; :: according to BINOP_1:def 2 :: thesis: f . (a,b) = f . (b,a)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;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

thus f . (a,b) = {} by A1, FUNCT_1:def 2

.= f . (b,a) by A1, FUNCT_1:def 2 ; :: thesis: verum