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;
then A5: C = the_inverseOp_wrt B by A1, A2, A3, FINSEQOP:def 3;

A6: now :: thesis: for f being Element of n -tuples_on D holds
( (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) )

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:113;
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:73 ; :: 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:73 ; :: 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 Th8;
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; :: thesis: verum