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