:: deftheorem defines := GRAPHSP:def 1 :
for i, k being Nat
for f being FinSequence of REAL
for r being Real holds (f,i) := (k,r) = (((f,i) := k),k) := r;