let F, G be Function of (TOP-REAL m),R^1; :: thesis: ( ( for p being Element of (TOP-REAL m) holds F . p = p /. n ) & ( for p being Element of (TOP-REAL m) holds G . p = p /. n ) implies F = G )
assume that
A2: for p being Element of (TOP-REAL m) holds F . p = p /. n and
A3: for p being Element of (TOP-REAL m) holds G . p = p /. n ; :: thesis: F = G
let p be Element of (TOP-REAL m); :: according to FUNCT_2:def 8 :: thesis: F . p = G . p
thus F . p = p /. n by A2
.= G . p by A3 ; :: thesis: verum