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