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

let 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;

hence F [;] ((G . (d1,d2)),f) = G .: ((F [;] (d1,f)),(F [;] (d2,f))) by FUNCT_2:63; :: thesis: verum