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