theorem Th33: :: BSPACE:33

for X being non empty set
for s being FinSequence of (bspace X)
for f being Element of (bspace X)
for x being Element of X holds (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*>