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 st n + 1 = len f & n + 1 in X holds
SignGen (f,B,X) = (SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>
let X be set ; :: thesis: for D being non empty set
for B being BinOp of D
for f being FinSequence of D st n + 1 = len f & n + 1 in X holds
SignGen (f,B,X) = (SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>
let D be non empty set ; :: thesis: for B being BinOp of D
for f being FinSequence of D st n + 1 = len f & n + 1 in X holds
SignGen (f,B,X) = (SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>
let B be BinOp of D; :: thesis: for f being FinSequence of D st n + 1 = len f & n + 1 in X holds
SignGen (f,B,X) = (SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>
let f be FinSequence of D; :: thesis: ( n + 1 = len f & n + 1 in X implies SignGen (f,B,X) = (SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*> )
set n1 = n + 1;
set I = (the_inverseOp_wrt B) . (f . (n + 1));
assume A1: ( n + 1 = len f & n + 1 in X ) ; :: thesis: SignGen (f,B,X) = (SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>
n <= n + 1 by NAT_1:13;
then A2: len (f | n) = n by A1, FINSEQ_1:59;
then A3: ( len (SignGen ((f | n),B,X)) = n & len <*((the_inverseOp_wrt B) . (f . (n + 1)))*> = 1 & len (SignGen (f,B,X)) = len f ) by CARD_1:def 7;
A4: SignGen ((f | n),B,X) = (SignGen (f,B,X)) | n by Th72;
for i being Nat st 1 <= i & i <= len (SignGen (f,B,X)) holds
(SignGen (f,B,X)) . i = ((SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (SignGen (f,B,X)) implies (SignGen (f,B,X)) . i = ((SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>) . i )
assume A5: ( 1 <= i & i <= len (SignGen (f,B,X)) ) ; :: thesis: (SignGen (f,B,X)) . i = ((SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>) . i
len ((SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>) = n + 1 by A2, CARD_1:def 7;
then A6: ( i in dom ((SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>) & i in dom (SignGen (f,B,X)) ) by A1, A3, A5, FINSEQ_3:25;

per cases then ( i in dom (SignGen ((f | n),B,X)) or ex j being Nat st
( j in dom <*((the_inverseOp_wrt B) . (f . (n + 1)))*> & i = (len (SignGen ((f | n),B,X))) + j ) ) by FINSEQ_1:25;

suppose A7: i in dom (SignGen ((f | n),B,X)) ; :: thesis: (SignGen (f,B,X)) . i = ((SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>) . i

hence ((SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>) . i = (SignGen ((f | n),B,X)) . i by FINSEQ_1:def 7
.= (SignGen (f,B,X)) . i by A4, A7, FUNCT_1:47 ;
:: thesis: verum

end;

suppose ex j being Nat st
( j in dom <*((the_inverseOp_wrt B) . (f . (n + 1)))*> & i = (len (SignGen ((f | n),B,X))) + j ) ; :: thesis: (SignGen (f,B,X)) . i = ((SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>) . i

then consider j being Nat such that
A8: ( j in dom <*((the_inverseOp_wrt B) . (f . (n + 1)))*> & i = (len (SignGen ((f | n),B,X))) + j ) ;
j in {1} by A8, FINSEQ_1:2, FINSEQ_1:def 8;
then j = 1 by TARSKI:def 1;
hence ((SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>) . i = (SignGen (f,B,X)) . i by Def11, A6, A1, A8, A3; :: thesis: verum

end;

end;

end;

hence SignGen (f,B,X) = (SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*> by A1, A3, FINSEQ_1:22; :: thesis: verum