let C, D be non empty set ; :: thesis: for B being Element of Fin C
for F, G being BinOp of D
for f, f9 being Function of C,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 $$ B,f),(F $$ B,f9) = F $$ B,(G .: f,f9)
let B be Element of Fin C; :: thesis: for F, G being BinOp of D
for f, f9 being Function of C,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 $$ B,f),(F $$ B,f9) = F $$ B,(G .: f,f9)
let F, G be BinOp of D; :: thesis: for f, f9 being Function of C,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 $$ B,f),(F $$ B,f9) = F $$ B,(G .: f,f9)
let f, f9 be Function of C,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 $$ B,f),(F $$ B,f9) = F $$ B,(G .: f,f9) )
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 $$ B,f),(F $$ B,f9) = F $$ B,(G .: f,f9)
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:91, FINSEQOP:94;
hence G . (F $$ B,f),(F $$ B,f9) = F $$ B,(G .: f,f9) by A1, Th11; :: thesis: verum