theorem Th3: :: ANALMETR:3

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