theorem Th57: :: POLYNOM9:57

for L being doubleLoopStr
for f, e being FinSequence
for x being object
for E being set st len f = len e & not x in E holds
SgnMembershipNumber ((f ^ <*x*>),L,(e ^ <*E*>)) = SgnMembershipNumber (f,L,e)