:: deftheorem defines UnusedVx GRAPHSP:def 8 :
for f being Element of REAL *
for n being Nat holds UnusedVx (f,n) = { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } ;