let A be set ; :: thesis: for D being non empty set
for o being BinOp of D
for f, g being Function of A,D st o is commutative holds
o .: f,g = o .: g,f
let D be non empty set ; :: thesis: for o being BinOp of D
for f, g being Function of A,D st o is commutative holds
o .: f,g = o .: g,f
let o be BinOp of D; :: thesis: for f, g being Function of A,D st o is commutative holds
o .: f,g = o .: g,f
let f, g be Function of A,D; :: thesis: ( o is commutative implies o .: f,g = o .: g,f )
assume A1: for a, b being Element of D holds o . a,b = o . b,a ; :: according to BINOP_1:def 13 :: thesis: o .: f,g = o .: g,f
A2: ( dom (o .: f,g) = A & dom (o .: g,f) = A & dom f = A & rng f c= D & dom g = A & rng g c= D ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in A implies (o .: f,g) . x = (o .: g,f) . x )
assume A3: x in A ; :: thesis: (o .: f,g) . x = (o .: g,f) . x
then ( f . x in rng f & g . x in rng g ) by A2, FUNCT_1:def 5;
then reconsider a = f . x, b = g . x as Element of D ;
thus (o .: f,g) . x = o . a,b by A2, A3, FUNCOP_1:28
.= o . b,a by A1
.= (o .: g,f) . x by A2, A3, FUNCOP_1:28 ; :: thesis: verum

end;

hence o .: f,g = o .: g,f by A2, FUNCT_1:9; :: thesis: verum