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

r in REAL

then A2:
{ ||.x.|| where x is VECTOR of V : x in v + W } c= REAL
;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;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

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