let C, D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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
; :: thesis: F [;] (G . d1,d2),f = G .: (F [;] d1,f),(F [;] d2,f)
now let c be
Element of
C;
:: thesis: (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:66
.=
G . (F . d1,(f . c)),
(F . d2,(f . c))
by A1, BINOP_1:23
.=
G . ((F [;] d1,f) . c),
(F . d2,(f . c))
by FUNCOP_1:66
.=
G . ((F [;] d1,f) . c),
((F [;] d2,f) . c)
by FUNCOP_1:66
.=
(G .: (F [;] d1,f),(F [;] d2,f)) . c
by FUNCOP_1:48
;
:: thesis: verum end;
hence
F [;] (G . d1,d2),f = G .: (F [;] d1,f),(F [;] d2,f)
by FUNCT_2:113; :: thesis: verum