theorem :: ANALORT:52

for V being RealLinearSpace
for x, y being VECTOR of V
for uu being object holds
( uu is Element of (CESpace (V,x,y)) iff uu is VECTOR of V ) ;