theorem :: ANALORT:53

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