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 ) and
A2: F is having_a_unity and
A3: e = the_unity_wrt F and
A4: G . e,e = e and
A5: 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
A6: len p = len q ; :: thesis: G . (F "**" p),(F "**" q) = F "**" (G .: p,q)
A7: len p = len (G .: p,q) by A6, FINSEQ_2:86;
A8: ( dom p = Seg (len p) & dom q = Seg (len q) ) by FINSEQ_1:def 3;
A9: dom (G .: p,q) = Seg (len (G .: p,q)) by FINSEQ_1:def 3;
thus G . (F "**" p),(F "**" q) = G . (F $$ (findom p),([#] p,e)),(F "**" q) by A1, A2, A3, Def2
.= G . (F $$ (findom p),([#] p,e)),(F $$ (findom q),([#] q,e)) by A1, A2, A3, Def2
.= F $$ (findom p),(G .: ([#] p,e),([#] q,e)) by A1, A2, A3, A4, A5, A6, A8, Th11
.= F $$ (findom (G .: p,q)),([#] (G .: p,q),e) by A4, A6, A7, A8, A9, Lm4
.= F "**" (G .: p,q) by A1, A2, A3, Def2 ; :: thesis: verum