let D be non empty set ; :: thesis: for B being BinOp of D
for d 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 or len f >= 1 ) & 1 + (len f) in meet F holds
B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d))
let B be BinOp of D; :: thesis: for d 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 or len f >= 1 ) & 1 + (len f) in meet F holds
B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d))
let d 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 or len f >= 1 ) & 1 + (len f) in meet F holds
B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d))
let f be FinSequence of D; :: thesis: for F being finite set
for E being Enumeration of F st ( B is having_a_unity or len f >= 1 ) & 1 + (len f) in meet F holds
B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d))
let F be finite set ; :: thesis: for E being Enumeration of F st ( B is having_a_unity or len f >= 1 ) & 1 + (len f) in meet F holds
B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d))
let E be Enumeration of F; :: thesis: ( ( B is having_a_unity or len f >= 1 ) & 1 + (len f) in meet F implies B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d)) )
assume that
A1: ( B is having_a_unity or len f >= 1 ) and
A2: 1 + (len f) in meet F ; :: thesis: B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d))
set fd = f ^ <*d*>;
set C = SignGenOp (f,B,F);
set Cd = SignGenOp ((f ^ <*d*>),B,F);
set I = the_inverseOp_wrt B;
( len ((SignGenOp ((f ^ <*d*>),B,F)) * E) = len E & len E = len ((SignGenOp (f,B,F)) * E) ) by CARD_1:def 7;
then A3: ( dom ((SignGenOp ((f ^ <*d*>),B,F)) * E) = dom E & dom E = dom ((SignGenOp (f,B,F)) * E) ) by FINSEQ_3:30;
A4: dom (B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E)) = dom ((SignGenOp ((f ^ <*d*>),B,F)) * E) by FUNCT_2:def 1;
for x being object st x in dom ((SignGenOp (f,B,F)) * E) holds
(B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d))) . x = (B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E)) . x

proof

let x be object ; :: thesis: ( x in dom ((SignGenOp (f,B,F)) * E) implies (B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d))) . x = (B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E)) . x )
assume A5: x in dom ((SignGenOp (f,B,F)) * E) ; :: thesis: (B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d))) . x = (B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E)) . x
( E . x in rng E & rng E = F ) by A5, A3, FUNCT_1:def 3, RLAFFIN3:def 1;
then A6: 1 + (len f) in E . x by A2, SETFAM_1:def 1;
A7: ( (f ^ <*d*>) . ((len f) + 1) = d & (f ^ <*d*>) | (len f) = f & len (f ^ <*d*>) = (len f) + 1 ) by FINSEQ_2:16;
A8: dom (B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d))) = dom ((SignGenOp (f,B,F)) * E) by FUNCT_2:def 1;
A9: len (SignGen (f,B,(E . x))) = len f by CARD_1:def 7;
A10: ((SignGenOp (f,B,F)) * E) . x = SignGen (f,B,(E . x)) by A5, Th80;
((SignGenOp ((f ^ <*d*>),B,F)) * E) . x = SignGen ((f ^ <*d*>),B,(E . x)) by A5, A3, Th80;
hence (B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E)) . x = B "**" (SignGen ((f ^ <*d*>),B,(E . x))) by A3, A5, Def10
.= B "**" ((SignGen (f,B,(E . x))) ^ <*((the_inverseOp_wrt B) . d)*>) by A7, Th73, A6
.= B . ((B "**" (SignGen (f,B,(E . x)))),((the_inverseOp_wrt B) . d)) by A9, A1, FINSOP_1:4
.= B . (((B "**" ((SignGenOp (f,B,F)) * E)) . x),((the_inverseOp_wrt B) . d)) by A10, A5, Def10
.= (B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d))) . x by A5, A8, FUNCOP_1:27 ;
:: thesis: verum

end;

hence B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d)) by FUNCT_2:def 1, A3, A4; :: thesis: verum