let D be non empty set ; :: thesis: for d being Element of D
for F, G being BinOp of D
for p being FinSequence of 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 "**" p),d = F "**" (G [:] p,d)
let d be Element of D; :: thesis: for F, G being BinOp of D
for p being FinSequence of 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 "**" p),d = F "**" (G [:] p,d)
let F, G be BinOp of D; :: thesis: for p being FinSequence of 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 "**" p),d = F "**" (G [:] p,d)
let p be FinSequence of 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 "**" p),d = F "**" (G [:] p,d) )
assume A1: ( F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F ) ; :: thesis: G . (F "**" p),d = F "**" (G [:] p,d)
set e = the_unity_wrt F;
G . (the_unity_wrt F),d = the_unity_wrt F by A1, FINSEQOP:70;
hence G . (F "**" p),d = F "**" (G [:] p,d) by A1, Th50; :: thesis: verum