theorem Th10: :: HILB10_4:10

for f1, f2 being XFinSequence
for n being Nat st n <= len f1 holds
(f1 ^ f2) /^ n = (f1 /^ n) ^ f2