theorem Th9: :: NUMERAL2:9

for F being XFinSequence
for X, Y being set st X misses Y holds
ex P being Permutation of (dom (SubXFinS (F,(X \/ Y)))) st (SubXFinS (F,(X \/ Y))) * P = (SubXFinS (F,X)) ^ (SubXFinS (F,Y))