P ** R is ManySortedFunction of bool M, bool M ;
hence P ** R is MSSetOp of M ; :: thesis: verum