let D be non empty set ; :: thesis: for d being Element of D
for G, F 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 G, F 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 G, F 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:66
.= G . d,(F . d1,d2) by FUNCT_1:35
.= F . (G . d,d1),(G . d,d2) by A1, BINOP_1:23
.= F . (G . d,((id D) . d1)),(G . d,d2) by FUNCT_1:35
.= F . (G . d,((id D) . d1)),(G . d,((id D) . d2)) by FUNCT_1:35
.= F . (u . d1),(G . d,((id D) . d2)) by A2, FUNCOP_1:66
.= F . (u . d1),(u . d2) by A2, FUNCOP_1:66 ; :: thesis: verum