theorem :: BSPACE:1

for S being 1-sorted
for i being Element of NAT
for p being FinSequence of S st i in dom p holds
p . i in S