let D be non empty set ; :: thesis: for e being Element of D
for F, G being BinOp of D
for p, q being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . e,e = e & ( for d1, d2, d3, d4 being Element of D holds F . (G . d1,d2),(G . d3,d4) = G . (F . d1,d3),(F . d2,d4) ) & len p = len q holds
G . (F "**" p),(F "**" q) = F "**" (G .: p,q)
let e be Element of D; :: thesis: for F, G being BinOp of D
for p, q being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . e,e = e & ( for d1, d2, d3, d4 being Element of D holds F . (G . d1,d2),(G . d3,d4) = G . (F . d1,d3),(F . d2,d4) ) & len p = len q holds
G . (F "**" p),(F "**" q) = F "**" (G .: p,q)
let F, G be BinOp of D; :: thesis: for p, q being FinSequence of D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . e,e = e & ( for d1, d2, d3, d4 being Element of D holds F . (G . d1,d2),(G . d3,d4) = G . (F . d1,d3),(F . d2,d4) ) & len p = len q holds
G . (F "**" p),(F "**" q) = F "**" (G .: p,q)
let p, q be FinSequence of D; :: thesis: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . e,e = e & ( for d1, d2, d3, d4 being Element of D holds F . (G . d1,d2),(G . d3,d4) = G . (F . d1,d3),(F . d2,d4) ) & len p = len q implies G . (F "**" p),(F "**" q) = F "**" (G .: p,q) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F ) and
A2: G . e,e = e and
A3: for d1, d2, d3, d4 being Element of D holds F . (G . d1,d2),(G . d3,d4) = G . (F . d1,d3),(F . d2,d4) and
A4: len p = len q ; :: thesis: G . (F "**" p),(F "**" q) = F "**" (G .: p,q)
A5: len p = len (G .: p,q) by A4, FINSEQ_2:86;
A6: dom (G .: p,q) = Seg (len (G .: p,q)) by FINSEQ_1:def 3;
A7: dom q = Seg (len q) by FINSEQ_1:def 3;
A8: dom p = Seg (len p) by FINSEQ_1:def 3;
thus G . (F "**" p),(F "**" q) = G . (F $$ (findom p),([#] p,e)),(F "**" q) by A1, Def2
.= G . (F $$ (findom p),([#] p,e)),(F $$ (findom q),([#] q,e)) by A1, Def2
.= F $$ (findom p),(G .: ([#] p,e),([#] q,e)) by A1, A2, A3, A4, A8, A7, Th11
.= F $$ (findom (G .: p,q)),([#] (G .: p,q),e) by A2, A4, A5, A8, A6, Lm4
.= F "**" (G .: p,q) by A1, Def2 ; :: thesis: verum