theorem Th48: :: SETLIM_1:48

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