let n be Nat; :: thesis: for D being non empty set
for B being BinOp of D
for C being UnOp of D st B is having_a_unity & B is associative & C is_an_inverseOp_wrt B holds
product C,n is_an_inverseOp_wrt product B,n
let D be non empty set ; :: thesis: for B being BinOp of D
for C being UnOp of D st B is having_a_unity & B is associative & C is_an_inverseOp_wrt B holds
product C,n is_an_inverseOp_wrt product B,n
let B be BinOp of D; :: thesis: for C being UnOp of D st B is having_a_unity & B is associative & C is_an_inverseOp_wrt B holds
product C,n is_an_inverseOp_wrt product B,n
let C be UnOp of D; :: thesis: ( B is having_a_unity & B is associative & C is_an_inverseOp_wrt B implies product C,n is_an_inverseOp_wrt product B,n )
assume that
A1: B is having_a_unity and
A2: B is associative and
A3: C is_an_inverseOp_wrt B ; :: thesis: product C,n is_an_inverseOp_wrt product B,n
A4: B is having_an_inverseOp by A3, FINSEQOP:def 2;
then A5: C = the_inverseOp_wrt B by A1, A2, A3, FINSEQOP:def 3;

A6: now

let f be Element of n -tuples_on D; :: thesis: ( (product B,n) . f,((product C,n) . f) = n |-> (the_unity_wrt B) & (product B,n) . ((product C,n) . f),f = n |-> (the_unity_wrt B) )
reconsider f9 = f as Element of n -tuples_on D ;
reconsider cf = C * f9 as Element of n -tuples_on D by FINSEQ_2:133;
thus (product B,n) . f,((product C,n) . f) = (product B,n) . f9,(C * f9) by Def2
.= B .: f9,cf by Def1
.= n |-> (the_unity_wrt B) by A1, A2, A4, A5, FINSEQOP:77 ; :: thesis: (product B,n) . ((product C,n) . f),f = n |-> (the_unity_wrt B)
thus (product B,n) . ((product C,n) . f),f = (product B,n) . (C * f9),f9 by Def2
.= B .: cf,f9 by Def1
.= n |-> (the_unity_wrt B) by A1, A2, A4, A5, FINSEQOP:77 ; :: thesis: verum

end;

ex d being Element of D st d is_a_unity_wrt B by A1, SETWISEO:def 2;
then the_unity_wrt B is_a_unity_wrt B by BINOP_1:def 8;
then n |-> (the_unity_wrt B) is_a_unity_wrt product B,n by Th16;
then n |-> (the_unity_wrt B) = the_unity_wrt (product B,n) by BINOP_1:def 8;
hence product C,n is_an_inverseOp_wrt product B,n by A6, FINSEQOP:def 1; :: thesis: verum