theorem :: REAL_NS2:71

for V being RealLinearSpace
for F being set holds
( F is Function of V,REAL iff F is Function of (RLSp2RVSp V),REAL ) ;