let A be set ; 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 ; 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; 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; ( 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)
; BINOP_1:def 2 o .: (f,g) = o .: (g,f)
now for x being object st x in A holds
(o .: (f,g)) . x = (o .: (g,f)) . xlet x be
object ;
( x in A implies (o .: (f,g)) . x = (o .: (g,f)) . x )assume A5:
x in A
;
(o .: (f,g)) . x = (o .: (g,f)) . xthen
(
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
;
verum end;
hence
o .: (f,g) = o .: (g,f)
by A1, A3, FUNCT_1:2; verum