let D be non empty set ; 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; 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; 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; ( 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
; 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:84;
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, Th13
.=
F $$ ((findom p),([#] ((G [:] (p,d)),e)))
by A3, Lm5
.=
F "**" (G [:] (p,d))
by A1, A4, A5, Def2
; verum