theorem Th3: :: NUMBER08:3

for X being set
for f, g being FinSequence st f ^ g is X -valued holds
( f is X -valued & g is X -valued )