theorem Th73: :: HILB10_7:73

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