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 . (d,e) = e holds

G . (d,(F "**" p)) = F "**" (G [;] (d,p))

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 . (d,e) = e holds

G . (d,(F "**" p)) = F "**" (G [;] (d,p))

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 . (d,e) = e holds

G . (d,(F "**" p)) = F "**" (G [;] (d,p))

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 . (d,e) = e implies G . (d,(F "**" p)) = F "**" (G [;] (d,p)) )

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 . (d,e) = e ; :: thesis: G . (d,(F "**" p)) = F "**" (G [;] (d,p))

A4: ( len p = len (G [;] (d,p)) & Seg (len p) = dom p ) by FINSEQ_1:def 3, FINSEQ_2:78;

A5: Seg (len (G [;] (d,p))) = dom (G [;] (d,p)) by FINSEQ_1:def 3;

thus G . (d,(F "**" p)) = G . (d,(F $$ ((findom p),([#] (p,e))))) by A1, Def2

.= F $$ ((findom p),(G [;] (d,([#] (p,e))))) by A1, A2, A3, Th12

.= F $$ ((findom p),([#] ((G [;] (d,p)),e))) by A3, Lm6

.= F "**" (G [;] (d,p)) by A1, A4, A5, Def2 ; :: thesis: verum

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 . (d,e) = e holds

G . (d,(F "**" p)) = F "**" (G [;] (d,p))

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 . (d,e) = e holds

G . (d,(F "**" p)) = F "**" (G [;] (d,p))

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 . (d,e) = e holds

G . (d,(F "**" p)) = F "**" (G [;] (d,p))

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 . (d,e) = e implies G . (d,(F "**" p)) = F "**" (G [;] (d,p)) )

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 . (d,e) = e ; :: thesis: G . (d,(F "**" p)) = F "**" (G [;] (d,p))

A4: ( len p = len (G [;] (d,p)) & Seg (len p) = dom p ) by FINSEQ_1:def 3, FINSEQ_2:78;

A5: Seg (len (G [;] (d,p))) = dom (G [;] (d,p)) by FINSEQ_1:def 3;

thus G . (d,(F "**" p)) = G . (d,(F $$ ((findom p),([#] (p,e))))) by A1, Def2

.= F $$ ((findom p),(G [;] (d,([#] (p,e))))) by A1, A2, A3, Th12

.= F $$ ((findom p),([#] ((G [;] (d,p)),e))) by A3, Lm6

.= F "**" (G [;] (d,p)) by A1, A4, A5, Def2 ; :: thesis: verum