let X be non empty set ; :: thesis: for F being BinOp of X
for Y being set
for f, g being Function of Y,X
for x being Element of X st F is associative holds
F .: (F [;] x,f),g = F [;] x,(F .: f,g)
let F be BinOp of X; :: thesis: for Y being set
for f, g being Function of Y,X
for x being Element of X st F is associative holds
F .: (F [;] x,f),g = F [;] x,(F .: f,g)
let Y be set ; :: thesis: for f, g being Function of Y,X
for x being Element of X st F is associative holds
F .: (F [;] x,f),g = F [;] x,(F .: f,g)
let f, g be Function of Y,X; :: thesis: for x being Element of X st F is associative holds
F .: (F [;] x,f),g = F [;] x,(F .: f,g)
let x be Element of X; :: thesis: ( F is associative implies F .: (F [;] x,f),g = F [;] x,(F .: f,g) )
assume A1: F is associative ; :: thesis: F .: (F [;] x,f),g = F [;] x,(F .: f,g)

per cases ( Y = {} or Y <> {} ) ;

suppose Y = {} ; :: thesis: F .: (F [;] x,f),g = F [;] x,(F .: f,g)

hence F .: (F [;] x,f),g = F [;] x,(F .: f,g) ; :: thesis: verum

end;

suppose A2: Y <> {} ; :: thesis: F .: (F [;] x,f),g = F [;] x,(F .: f,g)

now

let y be Element of Y; :: thesis: (F [;] x,(F .: f,g)) . y = F . ((F [;] x,f) . y),(g . y)
reconsider x1 = f . y, x2 = g . y as Element of X by A2, FUNCT_2:7;
thus (F [;] x,(F .: f,g)) . y = F . x,((F .: f,g) . y) by A2, Th66
.= F . x,(F . x1,x2) by A2, Th48
.= F . (F . x,x1),x2 by A1, BINOP_1:def 3
.= F . ((F [;] x,f) . y),(g . y) by A2, Th66 ; :: thesis: verum

end;

hence F .: (F [;] x,f),g = F [;] x,(F .: f,g) by A2, Th49; :: thesis: verum

end;

end;