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)))

now :: thesis: for x being object st x in A holds
(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;

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