theorem :: FINSEQ_6:17

for f1, f2 being FinSequence
for p being set st f1 ^ f2 just_once_values p & p in rng f1 holds
f1 just_once_values p