the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence .: (pr2 ( the carrier of X, the carrier of Y)) is Function of (bool the carrier of [:X,Y:]),(bool the carrier of Y) ; :: thesis: verum