theorem :: FINSEQ_6:155

for D being non empty set
for f1 being non empty FinSequence of D
for f2 being FinSequence of D holds (f1 ^' f2) /. 1 = f1 /. 1