(rng [:X,Y:]) \ Y = {} ;
hence [:X,Y:] is Y -valued by Th29; :: thesis: verum