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