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 [:] f,(G . d1,d2) = G .: (F [:] f,d1),(F [:] f,d2)
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 [:] f,(G . d1,d2) = G .: (F [:] f,d1),(F [:] f,d2)
let f be Function of C,D; :: thesis: for F, G being BinOp of D st F is_distributive_wrt G holds
F [:] f,(G . d1,d2) = G .: (F [:] f,d1),(F [:] f,d2)
let F, G be BinOp of D; :: thesis: ( F is_distributive_wrt G implies F [:] f,(G . d1,d2) = G .: (F [:] f,d1),(F [:] f,d2) )
assume A1: F is_distributive_wrt G ; :: thesis: F [:] f,(G . d1,d2) = G .: (F [:] f,d1),(F [:] f,d2)

now

let c be Element of C; :: thesis: (F [:] f,(G . d1,d2)) . c = (G .: (F [:] f,d1),(F [:] f,d2)) . c
thus (F [:] f,(G . d1,d2)) . c = F . (f . c),(G . d1,d2) by FUNCOP_1:60
.= G . (F . (f . c),d1),(F . (f . c),d2) by A1, BINOP_1:23
.= G . ((F [:] f,d1) . c),(F . (f . c),d2) by FUNCOP_1:60
.= G . ((F [:] f,d1) . c),((F [:] f,d2) . c) by FUNCOP_1:60
.= (G .: (F [:] f,d1),(F [:] f,d2)) . c by FUNCOP_1:48 ; :: thesis: verum

end;

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