let C, D be non empty set ; for d1, d2 being Element of D
for f being Function of C,D
for F, G being BinOp of D st F is_distributive_wrt G holds
F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f)))
let d1, d2 be Element of D; for f being Function of C,D
for F, G being BinOp of D st F is_distributive_wrt G holds
F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f)))
let f be Function of C,D; for F, G being BinOp of D st F is_distributive_wrt G holds
F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f)))
let F, G be BinOp of D; ( F is_distributive_wrt G implies F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f))) )
assume A1:
F is_distributive_wrt G
; F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f)))
now for c being Element of C holds (F [;] ((G . (d1,d2)),f)) . c = (G .: ((F [;] (d1,f)),(F [;] (d2,f)))) . clet c be
Element of
C;
(F [;] ((G . (d1,d2)),f)) . c = (G .: ((F [;] (d1,f)),(F [;] (d2,f)))) . cthus (F [;] ((G . (d1,d2)),f)) . c =
F . (
(G . (d1,d2)),
(f . c))
by FUNCOP_1:53
.=
G . (
(F . (d1,(f . c))),
(F . (d2,(f . c))))
by A1, BINOP_1:11
.=
G . (
((F [;] (d1,f)) . c),
(F . (d2,(f . c))))
by FUNCOP_1:53
.=
G . (
((F [;] (d1,f)) . c),
((F [;] (d2,f)) . c))
by FUNCOP_1:53
.=
(G .: ((F [;] (d1,f)),(F [;] (d2,f)))) . c
by FUNCOP_1:37
;
verum end;
hence
F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f)))
by FUNCT_2:63; verum