let m, n be Element of NAT ; :: thesis: for f being Element of REAL * holds f,f equal_at m,n
let f be Element of REAL * ; :: thesis: f,f equal_at m,n
for k being Element of NAT st k in dom f & m <= k & k <= n holds
f . k = f . k ;
hence f,f equal_at m,n by Def16; :: thesis: verum