theorem NF120: :: BINPACK1:7

for a being non empty FinSequence of REAL
for p being set
for i being Nat st p \/ {i} c= dom a & ( for m being Nat st m in p holds
m < i ) holds
Seq (a | (p \/ {i})) = (Seq (a | p)) ^ <*(a . i)*>