let F, G be Function of T,(TOP-REAL n); :: thesis: ( ( for t being Element of T holds F . t = n |-> (f . t) ) & ( for t being Element of T holds G . t = n |-> (f . t) ) implies F = G )

assume that

A2: for t being Element of T holds F . t = n |-> (f . t) and

A3: for t being Element of T holds G . t = n |-> (f . t) ; :: thesis: F = G

let t be Element of T; :: according to FUNCT_2:def 8 :: thesis: F . t = G . t

thus F . t = n |-> (f . t) by A2

.= G . t by A3 ; :: thesis: verum

assume that

A2: for t being Element of T holds F . t = n |-> (f . t) and

A3: for t being Element of T holds G . t = n |-> (f . t) ; :: thesis: F = G

let t be Element of T; :: according to FUNCT_2:def 8 :: thesis: F . t = G . t

thus F . t = n |-> (f . t) by A2

.= G . t by A3 ; :: thesis: verum