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 :: thesis: for c being Element of C holds (F [:] (f,(G . (d1,d2)))) . c = (G .: ((F [:] (f,d1)),(F [:] (f,d2)))) . c
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:48
.= G . ((F . ((f . c),d1)),(F . ((f . c),d2))) by A1, BINOP_1:11
.= G . (((F [:] (f,d1)) . c),(F . ((f . c),d2))) by FUNCOP_1:48
.= G . (((F [:] (f,d1)) . c),((F [:] (f,d2)) . c)) by FUNCOP_1:48
.= (G .: ((F [:] (f,d1)),(F [:] (f,d2)))) . c by FUNCOP_1:37 ; :: thesis: verum
end;
hence F [:] (f,(G . (d1,d2))) = G .: ((F [:] (f,d1)),(F [:] (f,d2))) by FUNCT_2:63; :: thesis: verum