theorem Th6: :: FINSEQ_6:6

for f1, f2 being FinSequence
for p being set st p in rng f1 holds
p .. (f1 ^ f2) = p .. f1