the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:] by Def5;
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