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

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