let D be non empty set ; :: 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 & F is having_an_inverseOp & G = F * ((id D),(the_inverseOp_wrt F)) 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 & F is having_an_inverseOp & G = F * ((id D),(the_inverseOp_wrt F)) 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 & F is having_an_inverseOp & G = F * ((id D),(the_inverseOp_wrt F)) 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 & F is having_an_inverseOp & G = F * ((id D),(the_inverseOp_wrt F)) implies G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2)) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: ( F is having_an_inverseOp & G = F * ((id D),(the_inverseOp_wrt F)) ) ; :: thesis: G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2))
set e = the_unity_wrt F;
( G . ((the_unity_wrt F),(the_unity_wrt F)) = the_unity_wrt F & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) ) by A1, A2, FINSEQOP:86, FINSEQOP:89;
hence G . ((F "**" T1),(F "**" T2)) = F "**" (G .: (T1,T2)) by A1, Th33; :: thesis: verum