let D be non empty set ; :: thesis: for d, e 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 & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e holds
G . ((F "**" p),d) = F "**" (G [:] (p,d))

let d, e 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 & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e 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 & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e 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 & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e implies G . ((F "**" p),d) = F "**" (G [:] (p,d)) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F ) and
A2: G is_distributive_wrt F and
A3: G . (e,d) = e ; :: thesis: G . ((F "**" p),d) = F "**" (G [:] (p,d))
A4: ( len p = len (G [:] (p,d)) & Seg (len p) = dom p ) by ;
A5: Seg (len (G [:] (p,d))) = dom (G [:] (p,d)) by FINSEQ_1:def 3;
thus G . ((F "**" p),d) = G . ((F \$\$ ((),([#] (p,e)))),d) by
.= F \$\$ ((),(G [:] (([#] (p,e)),d))) by A1, A2, A3, Th13
.= F \$\$ ((),([#] ((G [:] (p,d)),e))) by
.= F "**" (G [:] (p,d)) by A1, A4, A5, Def2 ; :: thesis: verum