now :: thesis: for r being object st r in { ||.x.|| where x is VECTOR of V : x in v + W } holds
r in REAL

let r be object ; :: thesis: ( r in { ||.x.|| where x is VECTOR of V : x in v + W } implies r in REAL )
assume r in { ||.x.|| where x is VECTOR of V : x in v + W } ; :: thesis: r in REAL
then consider x being VECTOR of V such that
A1: ( r = ||.x.|| & x in v + W ) ;
thus r in REAL by A1; :: thesis: verum

end;

then A2: { ||.x.|| where x is VECTOR of V : x in v + W } c= REAL ;
v in v + W by RLSUB_1:43;
then ||.v.|| in { ||.x.|| where x is VECTOR of V : x in v + W } ;
hence { ||.x.|| where x is VECTOR of V : x in v + W } is non empty Subset of REAL by A2; :: thesis: verum