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;

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

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) )

ex d being Element of D st d is_a_unity_wrt B
by A1, SETWISEO:def 2;( (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;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

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