theorem :: FINSEQ_6:11

for f1, f2 being FinSequence
for A being set st A c= dom f1 holds
(f1 ^ f2) | A = f1 | A by Th10, GRFUNC_1:27;