theorem Th6: :: JORDAN4:6

for D being non empty set
for f1 being FinSequence of D
for k being Nat st k < len f1 holds
( (f1 /^ k) . (len (f1 /^ k)) = f1 . (len f1) & (f1 /^ k) /. (len (f1 /^ k)) = f1 /. (len f1) )