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 ;
A6: now :: thesis: for f being Element of n -tuples_on D holds
( (product (B,n)) . (f,((product (C,n)) . f)) = n |-> () & (product (B,n)) . (((product (C,n)) . f),f) = n |-> () )
let f be Element of n -tuples_on D; :: thesis: ( (product (B,n)) . (f,((product (C,n)) . f)) = n |-> () & (product (B,n)) . (((product (C,n)) . f),f) = n |-> () )
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 |-> () by ; :: thesis: (product (B,n)) . (((product (C,n)) . f),f) = n |-> ()
thus (product (B,n)) . (((product (C,n)) . f),f) = (product (B,n)) . ((C * f9),f9) by Def2
.= B .: (cf,f9) by Def1
.= n |-> () by ; :: thesis: verum
end;
ex d being Element of D st d is_a_unity_wrt B by ;
then the_unity_wrt B is_a_unity_wrt B by BINOP_1:def 8;
then n |-> () is_a_unity_wrt product (B,n) by Th8;
then n |-> () = 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