let D be non empty set ; for d being Element of D
for F, G being BinOp of D
for u being UnOp of D st G is_distributive_wrt F & u = G [;] (d,(id D)) holds
u is_distributive_wrt F
let d be Element of D; for F, G being BinOp of D
for u being UnOp of D st G is_distributive_wrt F & u = G [;] (d,(id D)) holds
u is_distributive_wrt F
let F, G be BinOp of D; for u being UnOp of D st G is_distributive_wrt F & u = G [;] (d,(id D)) holds
u is_distributive_wrt F
let u be UnOp of D; ( G is_distributive_wrt F & u = G [;] (d,(id D)) implies u is_distributive_wrt F )
assume that
A1:
G is_distributive_wrt F
and
A2:
u = G [;] (d,(id D))
; u is_distributive_wrt F
let d1 be Element of D; BINOP_1:def 20 for b1 being Element of D holds u . (F . (d1,b1)) = F . ((u . d1),(u . b1))
let d2 be Element of D; u . (F . (d1,d2)) = F . ((u . d1),(u . d2))
thus u . (F . (d1,d2)) =
G . (d,((id D) . (F . (d1,d2))))
by A2, FUNCOP_1:53
.=
G . (d,(F . (d1,d2)))
.=
F . ((G . (d,d1)),(G . (d,d2)))
by A1, BINOP_1:11
.=
F . ((G . (d,((id D) . d1))),(G . (d,d2)))
.=
F . ((G . (d,((id D) . d1))),(G . (d,((id D) . d2))))
.=
F . ((u . d1),(G . (d,((id D) . d2))))
by A2, FUNCOP_1:53
.=
F . ((u . d1),(u . d2))
by A2, FUNCOP_1:53
; verum