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