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 )
A1: dom (o .: f,g) = A by FUNCT_2:def 1;
A2: ( dom f = A & dom g = A ) by FUNCT_2:def 1;
A3: dom (o .: g,f) = A by FUNCT_2:def 1;
assume A4: 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

now

let x be set ; :: thesis: ( x in A implies (o .: f,g) . x = (o .: g,f) . x )
assume A5: 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 A1, A5, FUNCOP_1:28
.= o . b,a by A4
.= (o .: g,f) . x by A3, A5, FUNCOP_1:28 ; :: thesis: verum

end;

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