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
A2: for W being open Subset of [:X,Y:] holds F . W = W,the carrier of X *graph and
A3: for W being open Subset of [:X,Y:] holds G . W = W,the carrier of X *graph ; :: thesis: F = G

now

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 5;
thus F . x = W,the carrier of X *graph by A2
.= G . x by A3 ; :: thesis: verum

end;

hence F = G by FUNCT_2:113; :: thesis: verum