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 CARD_1:def 7;

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 Th32; :: thesis: verum

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 CARD_1:def 7;

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 Th32; :: thesis: verum