theorem :: SPPOL_2:44

for i being Nat
for f being S-Sequence_in_R2 st i in dom f holds
f /. i in L~ f