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