theorem LM060: :: PRSUBSET:3

for x being REAL -valued FinSequence
for i being Nat
for I0 being set st I0 c= Seg i & Seg (i + 1) c= dom x holds
Seq ((x | (i + 1)),(I0 \/ {(i + 1)})) = (Seq ((x | i),I0)) ^ <*(x . (i + 1))*>