theorem Th74: :: HILB10_7:74

for n being Nat
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 & not n + 1 in X holds
SignGen (f,B,X) = (SignGen ((f | n),B,X)) ^ <*(f . (n + 1))*>