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 . e,d = e holds
G . (F "**" p),d = F "**" (G [:] p,d)
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 . 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 FINSEQ_1:def 3, FINSEQ_2:98;
A5: Seg (len (G [:] p,d)) = dom (G [:] p,d) by FINSEQ_1:def 3;
thus G . (F "**" p),d = G . (F $$ (findom p),([#] p,e)),d by A1, Def2
.= F $$ (findom p),(G [:] ([#] p,e),d) by A1, A2, A3, Th15
.= F $$ (findom p),([#] (G [:] p,d),e) by A3, Lm5
.= F "**" (G [:] p,d) by A1, A4, A5, Def2 ; :: thesis: verum