let D be non empty set ; :: thesis: for e being Element of D
for F, G being BinOp of D
for i being Nat
for T1, T2 being Element of i -tuples_on 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) ) holds
G . (F "**" T1),(F "**" T2) = F "**" (G .: T1,T2)
let e be Element of D; :: thesis: for F, G being BinOp of D
for i being Nat
for T1, T2 being Element of i -tuples_on 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) ) holds
G . (F "**" T1),(F "**" T2) = F "**" (G .: T1,T2)
let F, G be BinOp of D; :: thesis: for i being Nat
for T1, T2 being Element of i -tuples_on 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) ) holds
G . (F "**" T1),(F "**" T2) = F "**" (G .: T1,T2)
let i be Nat; :: thesis: for T1, T2 being Element of i -tuples_on 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) ) holds
G . (F "**" T1),(F "**" T2) = F "**" (G .: T1,T2)
let T1, T2 be Element of i -tuples_on 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) ) implies G . (F "**" T1),(F "**" T2) = F "**" (G .: T1,T2) )
( len T1 = i & len T2 = i ) by FINSEQ_1:def 18;
hence ( 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) ) implies G . (F "**" T1),(F "**" T2) = F "**" (G .: T1,T2) ) by Th43; :: thesis: verum