let C, D be non empty set ; 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; 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; 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; 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; ( 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
; 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; verum