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:72;

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, Th9

.= 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

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:72;

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, Th9

.= 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