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

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

hence
F = G
by FUNCT_2:63; :: thesis: verumlet 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;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