theorem Th41: :: SETLIM_1:41

for X being set
for B being SetSequence of X
for n being Nat st B is V56() holds
(superior_setsequence B) . n = (superior_setsequence B) . (n + 1)