ex V being RealLinearSpace ex w, y being VECTOR of V st Gen w,y by Def1, FUNCSDOM:23;