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