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