let n be Nat; :: thesis: for X being set
for D being non empty set
for B being BinOp of D
for f being FinSequence of D holds SignGen ((f | n),B,X) = (SignGen (f,B,X)) | n
let X be set ; :: thesis: for D being non empty set
for B being BinOp of D
for f being FinSequence of D holds SignGen ((f | n),B,X) = (SignGen (f,B,X)) | n
let D be non empty set ; :: thesis: for B being BinOp of D
for f being FinSequence of D holds SignGen ((f | n),B,X) = (SignGen (f,B,X)) | n
let B be BinOp of D; :: thesis: for f being FinSequence of D holds SignGen ((f | n),B,X) = (SignGen (f,B,X)) | n
let f be FinSequence of D; :: thesis: SignGen ((f | n),B,X) = (SignGen (f,B,X)) | n
A1: ( len (SignGen ((f | n),B,X)) = len (f | n) & len (SignGen (f,B,X)) = len f ) by CARD_1:def 7;

per cases ( n >= len f or n < len f ) ;

suppose n >= len f ; :: thesis: SignGen ((f | n),B,X) = (SignGen (f,B,X)) | n

then ( f | n = f & (SignGen (f,B,X)) | n = SignGen (f,B,X) ) by FINSEQ_1:58, A1;
hence SignGen ((f | n),B,X) = (SignGen (f,B,X)) | n ; :: thesis: verum

end;

suppose n < len f ; :: thesis: SignGen ((f | n),B,X) = (SignGen (f,B,X)) | n

then A2: ( len (f | n) = n & len (SignGen ((f | n),B,X)) = n & len ((SignGen (f,B,X)) | n) = n ) by FINSEQ_1:59, A1;
for i being Nat st 1 <= i & i <= len (SignGen ((f | n),B,X)) holds
(SignGen ((f | n),B,X)) . i = ((SignGen (f,B,X)) | n) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (SignGen ((f | n),B,X)) implies (SignGen ((f | n),B,X)) . i = ((SignGen (f,B,X)) | n) . i )
assume A3: ( 1 <= i & i <= len (SignGen ((f | n),B,X)) ) ; :: thesis: (SignGen ((f | n),B,X)) . i = ((SignGen (f,B,X)) | n) . i
A4: ( i in dom (SignGen ((f | n),B,X)) & i in dom ((SignGen (f,B,X)) | n) ) by A3, A2, FINSEQ_3:25;
then A5: i in dom (SignGen (f,B,X)) by RELAT_1:57;

per cases ( i in X or not i in X ) ;

suppose A6: i in X ; :: thesis: (SignGen ((f | n),B,X)) . i = ((SignGen (f,B,X)) | n) . i

hence (SignGen ((f | n),B,X)) . i = (the_inverseOp_wrt B) . ((f | n) . i) by Def11, A4
.= (the_inverseOp_wrt B) . (f . i) by A2, A3, FINSEQ_3:112
.= (SignGen (f,B,X)) . i by Def11, A5, A6
.= ((SignGen (f,B,X)) | n) . i by A4, FUNCT_1:47 ;
:: thesis: verum

end;

suppose A7: not i in X ; :: thesis: (SignGen ((f | n),B,X)) . i = ((SignGen (f,B,X)) | n) . i

hence (SignGen ((f | n),B,X)) . i = (f | n) . i by Def11, A4
.= f . i by A2, A3, FINSEQ_3:112
.= (SignGen (f,B,X)) . i by Def11, A5, A7
.= ((SignGen (f,B,X)) | n) . i by A4, FUNCT_1:47 ;
:: thesis: verum

end;

end;

end;

hence SignGen ((f | n),B,X) = (SignGen (f,B,X)) | n by A2; :: thesis: verum

end;

end;