theorem Th45: :: SETLIM_1:45

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