theorem Th133: :: HILB10_7:133

for D being non empty set
for A being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1
for CE1, CE2 being b₁ * -valued FinSequence st CE1 = (SignGenOp ((f ^ <*d1*>),A,F1)) * E1 & CE2 = (SignGenOp ((f ^ <*d2*>),A,F1)) * E1 holds
for s being FinSequence st s in doms CE1 & not 1 + (len f) in rng s holds
( s in doms CE2 & (App CE1) . s = (App CE2) . s )