theorem Th78: :: HILB10_7:78

for X being set
for D being non empty set
for B being BinOp of D
for f being FinSequence of D
for E being Enumeration of {X} holds (SignGenOp (f,B,{X})) * E = <*(SignGen (f,B,X))*>