theorem Th42: :: GRAPHSP:42

for m, n being Nat
for f being Element of REAL * holds f,f equal_at m,n ;