:: deftheorem defines equal_at GRAPHSP:def 16 :
for f, g being Element of REAL *
for m, n being Nat holds
( f,g equal_at m,n iff ( dom f = dom g & ( for k being Nat st k in dom f & m <= k & k <= n holds
f . k = g . k ) ) );