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 ) & not 1 + (len f) in union F holds
B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),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 ) & not 1 + (len f) in union F holds
B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),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 ) & not 1 + (len f) in union F holds
B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),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 ) & not 1 + (len f) in union F holds
B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),d)
let F be finite set ; :: thesis: for E being Enumeration of F st ( B is having_a_unity or len f >= 1 ) & not 1 + (len f) in union F holds
B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),d)
let E be Enumeration of F; :: thesis: ( ( B is having_a_unity or len f >= 1 ) & not 1 + (len f) in union F implies B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),d) )
assume that
A1: ( B is having_a_unity or len f >= 1 ) and
A2: not 1 + (len f) in union F ; :: thesis: B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),d)
set fd = f ^ <*d*>;
set C = SignGenOp (f,B,F);
set Cd = SignGenOp ((f ^ <*d*>),B,F);
( 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)),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)),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)),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: not 1 + (len f) in E . x by A2, TARSKI:def 4;
A7: (f ^ <*d*>) . ((len f) + 1) = d ;
A8: (f ^ <*d*>) | (len f) = f ;
A9: len (f ^ <*d*>) = (len f) + 1 by FINSEQ_2:16;
A10: dom (B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),d)) = dom ((SignGenOp (f,B,F)) * E) by FUNCT_2:def 1;
A11: len (SignGen (f,B,(E . x))) = len f by CARD_1:def 7;
A12: ((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))) ^ <*d*>) by A9, Th74, A6, A8, A7
.= B . ((B "**" (SignGen (f,B,(E . x)))),d) by A11, A1, FINSOP_1:4
.= B . (((B "**" ((SignGenOp (f,B,F)) * E)) . x),d) by A12, A5, Def10
.= (B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),d)) . x by A5, A10, FUNCOP_1:27 ;
:: thesis: verum

end;

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