theorem Th58: :: POLYNOM9:58
for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for f, e being FinSequence
for x being object
for E being set st len f = len e & x in E holds
SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = - (SgnMembershipNumber (f,L,e))