the carrier of W c= the carrier of V1 by VECTSP_4:def 2;
hence f | W is Function of W,V2 by FUNCT_2:32; :: thesis: verum