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

now

let x be set ; :: 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 5;
( f . x in rng f & g . x in rng g ) by A3, A8, FUNCT_1:def 5;
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:28
.= o . (o . a,b),c by A1, A8, FUNCOP_1:28
.= o . a,(o . b,c) by A7
.= o . a,((o .: g,h) . x) by A2, A8, FUNCOP_1:28
.= (o .: f,(o .: g,h)) . x by A6, A8, FUNCOP_1:28 ; :: thesis: verum

end;

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