let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: u is_distributive_wrt F
let d1 be Element of D; :: according to BINOP_1:def 20 :: thesis: for b₁ being Element of D holds u . (F . (d1,b₁)) = F . ((u . d1),(u . b₁))
let d2 be Element of D; :: thesis: 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 ; :: thesis: verum