theorem Th3: :: GRAPHSP:3

for X being set
for p being FinSequence of X
for ii being Integer st 1 <= ii & ii <= len p holds
p /. ii = p . ii