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)

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

hence
o .: (f,g) = o .: (g,f)
by A1, A3, FUNCT_1:2; :: thesis: verum(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;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