let D be non empty set ; :: thesis: for e, 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 & e = the_unity_wrt F & G is_distributive_wrt F & G . d,e = e holds
G . d,(F "**" p) = F "**" (G [;] d,p)
let e, 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 & 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 ) and
A2: e = the_unity_wrt F and
A3: G is_distributive_wrt F and
A4: G . d,e = e ; :: thesis: G . d,(F "**" p) = F "**" (G [;] d,p)
A5: len p = len (G [;] d,p) by FINSEQ_2:92;
A6: ( Seg (len p) = dom p & 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, A2, Def2
.= F $$ (findom p),(G [;] d,([#] p,e)) by A1, A2, A3, A4, Th14
.= F $$ (findom p),([#] (G [;] d,p),e) by A4, Lm6
.= F "**" (G [;] d,p) by A1, A2, A5, A6, Def2 ; :: thesis: verum