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 . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) )

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 . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

set e = the_unity_wrt F;

G . (d,(the_unity_wrt F)) = the_unity_wrt F by A1, A2, A3, FINSEQOP:66;

hence G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) by A1, A3, Th12; :: thesis: verum

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 . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) )

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 . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

set e = the_unity_wrt F;

G . (d,(the_unity_wrt F)) = the_unity_wrt F by A1, A2, A3, FINSEQOP:66;

hence G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) by A1, A3, Th12; :: thesis: verum