let F, G be Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))); :: thesis: ( ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) & ( for W being open Subset of [:X,Y:] holds G . W = (W, the carrier of X) *graph ) implies F = G )
assume that
A1: for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph and
A2: for W being open Subset of [:X,Y:] holds G . W = (W, the carrier of X) *graph ; :: thesis: F = G
now :: thesis: for x being Element of (InclPoset the topology of [:X,Y:]) holds F . x = G . x
let x be Element of (InclPoset the topology of [:X,Y:]); :: thesis: F . x = G . x
the carrier of (InclPoset the topology of [:X,Y:]) = the topology of [:X,Y:] by YELLOW_1:1;
then x in the topology of [:X,Y:] ;
then reconsider W = x as open Subset of [:X,Y:] by PRE_TOPC:def 2;
thus F . x = (W, the carrier of X) *graph by A1
.= G . x by A2 ; :: thesis: verum
end;
hence F = G by FUNCT_2:63; :: thesis: verum