let C, D be non empty set ; :: thesis: for B being Element of Fin C
for d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . ((F \$\$ (B,f)),d) = F \$\$ (B,(G [:] (f,d)))

let B be Element of Fin C; :: thesis: for d being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . ((F \$\$ (B,f)),d) = F \$\$ (B,(G [:] (f,d)))

let d be Element of D; :: thesis: for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . ((F \$\$ (B,f)),d) = F \$\$ (B,(G [:] (f,d)))

let F, G be BinOp of D; :: thesis: for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
G . ((F \$\$ (B,f)),d) = F \$\$ (B,(G [:] (f,d)))

let f be Function of C,D; :: thesis: ( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies G . ((F \$\$ (B,f)),d) = F \$\$ (B,(G [:] (f,d))) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: F is having_an_inverseOp and
A3: G is_distributive_wrt F ; :: thesis: G . ((F \$\$ (B,f)),d) = F \$\$ (B,(G [:] (f,d)))
set e = the_unity_wrt F;
G . ((),d) = the_unity_wrt F by ;
hence G . ((F \$\$ (B,f)),d) = F \$\$ (B,(G [:] (f,d))) by A1, A3, Th13; :: thesis: verum