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 ;
( f . x in rng f & g . x in rng g ) by ;
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
.= o . ((o . (a,b)),c) by
.= o . (a,(o . (b,c))) by A7
.= o . (a,((o .: (g,h)) . x)) by
.= (o .: (f,(o .: (g,h)))) . x by ; :: thesis: verum
end;
hence o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h))) by ; :: thesis: verum