let D be non empty set ; :: thesis: for B being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp & 1 + (len f) in meet F & 2 + (len f) in meet F holds
B "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),B,F)) * E) = B "**" ((SignGenOp ((f ^ <*(B . (d1,d2))*>),B,F)) * E)
let B be BinOp of D; :: thesis: for d1, d2 being Element of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp & 1 + (len f) in meet F & 2 + (len f) in meet F holds
B "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),B,F)) * E) = B "**" ((SignGenOp ((f ^ <*(B . (d1,d2))*>),B,F)) * E)
let d1, d2 be Element of D; :: thesis: for f being FinSequence of D
for F being finite set
for E being Enumeration of F st B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp & 1 + (len f) in meet F & 2 + (len f) in meet F holds
B "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),B,F)) * E) = B "**" ((SignGenOp ((f ^ <*(B . (d1,d2))*>),B,F)) * E)
let f be FinSequence of D; :: thesis: for F being finite set
for E being Enumeration of F st B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp & 1 + (len f) in meet F & 2 + (len f) in meet F holds
B "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),B,F)) * E) = B "**" ((SignGenOp ((f ^ <*(B . (d1,d2))*>),B,F)) * E)
let F be finite set ; :: thesis: for E being Enumeration of F st B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp & 1 + (len f) in meet F & 2 + (len f) in meet F holds
B "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),B,F)) * E) = B "**" ((SignGenOp ((f ^ <*(B . (d1,d2))*>),B,F)) * E)
set I = the_inverseOp_wrt B;
let E be Enumeration of F; :: thesis: ( B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp & 1 + (len f) in meet F & 2 + (len f) in meet F implies B "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),B,F)) * E) = B "**" ((SignGenOp ((f ^ <*(B . (d1,d2))*>),B,F)) * E) )
assume that
A1: ( B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp ) and
A2: ( 1 + (len f) in meet F & 2 + (len f) in meet F ) ; :: thesis: B "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),B,F)) * E) = B "**" ((SignGenOp ((f ^ <*(B . (d1,d2))*>),B,F)) * E)
A3: len (f ^ <*d1*>) = 1 + (len f) by FINSEQ_2:16;
then 1 + (len (f ^ <*d1*>)) in meet F by A2;
hence B "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp ((f ^ <*d1*>),B,F)) * E)),((the_inverseOp_wrt B) . d2)) by NAT_1:11, Th83, A3
.= B [:] ((B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d1))),((the_inverseOp_wrt B) . d2)) by A1, Th83, A2
.= B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),(B . (((the_inverseOp_wrt B) . d1),((the_inverseOp_wrt B) . d2)))) by A1, FUNCOP_1:63
.= B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . (B . (d1,((the_inverseOp_wrt B) . ((the_inverseOp_wrt B) . d2)))))) by A1, Th2
.= B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . (B . (d1,d2)))) by A1, FINSEQOP:62
.= B "**" ((SignGenOp ((f ^ <*(B . (d1,d2))*>),B,F)) * E) by A1, Th83, A2 ;
:: thesis: verum