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 2 :: thesis: o .: (f,g) = o .: (g,f)

now :: thesis: for x being object st x in A holds
(o .: (f,g)) . x = (o .: (g,f)) . x

let x be object ; :: 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 3;
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:22
.= o . (b,a) by A4
.= (o .: (g,f)) . x by A3, A5, FUNCOP_1:22 ; :: thesis: verum

end;

hence o .: (f,g) = o .: (g,f) by A1, A3, FUNCT_1:2; :: thesis: verum