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

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 <> {} )
;

end;

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

end;

now :: thesis: for y being Element of Y holds (F [;] (x,(F .: (f,g)))) . y = F . (((F [;] (x,f)) . y),(g . y))

hence
F .: ((F [;] (x,f)),g) = F [;] (x,(F .: (f,g)))
by A2, Th38; :: thesis: verumlet 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:5;

thus (F [;] (x,(F .: (f,g)))) . y = F . (x,((F .: (f,g)) . y)) by A2, Th53

.= F . (x,(F . (x1,x2))) by A2, Th37

.= F . ((F . (x,x1)),x2) by A1

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

end;reconsider x1 = f . y, x2 = g . y as Element of X by A2, FUNCT_2:5;

thus (F [;] (x,(F .: (f,g)))) . y = F . (x,((F .: (f,g)) . y)) by A2, Th53

.= F . (x,(F . (x1,x2))) by A2, Th37

.= F . ((F . (x,x1)),x2) by A1

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