theorem Lem8: :: BAGORD_2:7

for I being set
for p, q being FinSequence st p ^ q is I -valued holds
( p is I -valued & q is I -valued )