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 A1: ( B is having_a_unity & B is associative & C is_an_inverseOp_wrt B ) ; :: thesis: product C,n is_an_inverseOp_wrt product B,n
then A2: B is having_an_inverseOp by FINSEQOP:def 2;
then A3: C = the_inverseOp_wrt B by A1, FINSEQOP:def 3;
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 A4: n |-> (the_unity_wrt B) = the_unity_wrt (product B,n) by BINOP_1:def 8;

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 f' = f as Element of n -tuples_on D ;
reconsider cf = C * f' as Element of n -tuples_on D by FINSEQ_2:133;
thus (product B,n) . f,((product C,n) . f) = (product B,n) . f',(C * f') by Def2
.= B .: f',cf by Def1
.= n |-> (the_unity_wrt B) by A1, A2, A3, 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 * f'),f' by Def2
.= B .: cf,f' by Def1
.= n |-> (the_unity_wrt B) by A1, A2, A3, FINSEQOP:77 ; :: thesis: verum

end;

hence product C,n is_an_inverseOp_wrt product B,n by A4, FINSEQOP:def 1; :: thesis: verum