let A be set ; for D being non empty set
for o being BinOp of D
for f, g, h being Function of A,D st o is associative holds
o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h)))
let D be non empty set ; for o being BinOp of D
for f, g, h being Function of A,D st o is associative holds
o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h)))
let o be BinOp of D; for f, g, h being Function of A,D st o is associative holds
o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h)))
let f, g, h be Function of A,D; ( o is associative implies o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h))) )
A1:
dom (o .: (f,g)) = A
by FUNCT_2:def 1;
A2:
dom (o .: (g,h)) = A
by FUNCT_2:def 1;
A3:
( dom f = A & dom g = A )
by FUNCT_2:def 1;
A4:
dom (o .: ((o .: (f,g)),h)) = A
by FUNCT_2:def 1;
A5:
dom h = A
by FUNCT_2:def 1;
A6:
dom (o .: (f,(o .: (g,h)))) = A
by FUNCT_2:def 1;
assume A7:
for a, b, c being Element of D holds o . ((o . (a,b)),c) = o . (a,(o . (b,c)))
; BINOP_1:def 3 o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h)))
now for x being object st x in A holds
(o .: ((o .: (f,g)),h)) . x = (o .: (f,(o .: (g,h)))) . xlet x be
object ;
( x in A implies (o .: ((o .: (f,g)),h)) . x = (o .: (f,(o .: (g,h)))) . x )assume A8:
x in A
;
(o .: ((o .: (f,g)),h)) . x = (o .: (f,(o .: (g,h)))) . xthen A9:
h . x in rng h
by A5, FUNCT_1:def 3;
(
f . x in rng f &
g . x in rng g )
by A3, A8, FUNCT_1:def 3;
then reconsider a =
f . x,
b =
g . x,
c =
h . x as
Element of
D by A9;
thus (o .: ((o .: (f,g)),h)) . x =
o . (
((o .: (f,g)) . x),
c)
by A4, A8, FUNCOP_1:22
.=
o . (
(o . (a,b)),
c)
by A1, A8, FUNCOP_1:22
.=
o . (
a,
(o . (b,c)))
by A7
.=
o . (
a,
((o .: (g,h)) . x))
by A2, A8, FUNCOP_1:22
.=
(o .: (f,(o .: (g,h)))) . x
by A6, A8, FUNCOP_1:22
;
verum end;
hence
o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h)))
by A4, A6, FUNCT_1:2; verum