let X, Y be non empty TopSpace; :: thesis: for XT being Point of [:X,Y:] ex W being Point of X ex T being Point of Y st XT = [W,T]
let XT be Point of [:X,Y:]; :: thesis: ex W being Point of X ex T being Point of Y st XT = [W,T]
the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence ex W being Point of X ex T being Point of Y st XT = [W,T] by DOMAIN_1:1; :: thesis: verum