let X be non empty set ; for Y being set
for F being BinOp of X
for f, g being Function of Y,X
for x being Element of X st F is associative holds
F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g)))
let Y be set ; for F being BinOp of X
for f, g being Function of Y,X
for x being Element of X st F is associative holds
F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g)))
let F be BinOp of X; for f, g being Function of Y,X
for x being Element of X st F is associative holds
F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g)))
let f, g be Function of Y,X; for x being Element of X st F is associative holds
F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g)))
let x be Element of X; ( F is associative implies F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g))) )
assume A1:
F is associative
; F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g)))
per cases
( Y = {} or Y <> {} )
;
suppose A2:
Y <> {}
;
F .: ((F [:] (f,x)),g) = F .: (f,(F [;] (x,g)))now for y being Element of Y holds (F .: ((F [:] (f,x)),g)) . y = F . ((f . y),((F [;] (x,g)) . y))let y be
Element of
Y;
(F .: ((F [:] (f,x)),g)) . y = F . ((f . y),((F [;] (x,g)) . y))reconsider x1 =
f . y,
x2 =
g . y as
Element of
X by A2, FUNCT_2:5;
thus (F .: ((F [:] (f,x)),g)) . y =
F . (
((F [:] (f,x)) . y),
(g . y))
by A2, Th37
.=
F . (
(F . (x1,x)),
x2)
by A2, Th48
.=
F . (
x1,
(F . (x,x2)))
by A1
.=
F . (
(f . y),
((F [;] (x,g)) . y))
by A2, Th53
;
verum end; hence
F .: (
(F [:] (f,x)),
g)
= F .: (
f,
(F [;] (x,g)))
by A2, Th38;
verum end; end;