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