let X be non empty set ; :: thesis: for Y being set
for F being BinOp of X
for f, g being Function of Y,X st F is commutative holds
F .: (f,g) = F .: (g,f)
let Y be set ; :: thesis: for F being BinOp of X
for f, g being Function of Y,X st F is commutative holds
F .: (f,g) = F .: (g,f)
let F be BinOp of X; :: thesis: for f, g being Function of Y,X st F is commutative holds
F .: (f,g) = F .: (g,f)
let f, g be Function of Y,X; :: thesis: ( F is commutative implies F .: (f,g) = F .: (g,f) )
assume A1: F is commutative ; :: thesis: F .: (f,g) = F .: (g,f)

per cases ( Y = {} or Y <> {} ) ;

suppose Y = {} ; :: thesis: F .: (f,g) = F .: (g,f)

hence F .: (f,g) = F .: (g,f) ; :: thesis: verum

end;

suppose A2: Y <> {} ; :: thesis: F .: (f,g) = F .: (g,f)

now :: thesis: for y being Element of Y holds (F .: (f,g)) . y = F . ((g . y),(f . y))

let y be Element of Y; :: thesis: (F .: (f,g)) . y = F . ((g . y),(f . y))
reconsider x1 = f . y, x2 = g . y as Element of X by A2, FUNCT_2:5;
thus (F .: (f,g)) . y = F . (x1,x2) by A2, Th37
.= F . ((g . y),(f . y)) by A1 ; :: thesis: verum

end;

hence F .: (f,g) = F .: (g,f) by A2, Th38; :: thesis: verum

end;

end;