let A be set ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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))) ; :: according to BINOP_1:def 3 :: thesis: o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h)))

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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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))) ; :: according to BINOP_1:def 3 :: thesis: o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h)))

now :: thesis: for x being object st x in A holds

(o .: ((o .: (f,g)),h)) . x = (o .: (f,(o .: (g,h)))) . x

hence
o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h)))
by A4, A6, FUNCT_1:2; :: thesis: verum(o .: ((o .: (f,g)),h)) . x = (o .: (f,(o .: (g,h)))) . x

let x be object ; :: thesis: ( x in A implies (o .: ((o .: (f,g)),h)) . x = (o .: (f,(o .: (g,h)))) . x )

assume A8: x in A ; :: thesis: (o .: ((o .: (f,g)),h)) . x = (o .: (f,(o .: (g,h)))) . x

then 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 ; :: thesis: verum

end;assume A8: x in A ; :: thesis: (o .: ((o .: (f,g)),h)) . x = (o .: (f,(o .: (g,h)))) . x

then 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 ; :: thesis: verum