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)))

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 :: thesis: for c being Element of C holds (F [;] ((G . (d1,d2)),f)) . c = (G .: ((F [;] (d1,f)),(F [;] (d2,f)))) . c

hence
F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f)))
by FUNCT_2:63; :: thesis: verumlet c be Element of C; :: thesis: (F [;] ((G . (d1,d2)),f)) . c = (G .: ((F [;] (d1,f)),(F [;] (d2,f)))) . c

thus (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 ; :: thesis: verum

end;thus (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 ; :: thesis: verum