let V be RealLinearSpace; :: thesis: Up ((Omega). V) is circled
let u be VECTOR of V; :: according to CIRCLED1:def 1 :: thesis: for r being Real st |.r.| <= 1 & u in Up ((Omega). V) holds
r * u in Up ((Omega). V)
let r be Real; :: thesis: ( |.r.| <= 1 & u in Up ((Omega). V) implies r * u in Up ((Omega). V) )
(Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the U6 of V, the Mult of V #) by RLSUB_1:def 4;
then r * u in the carrier of ((Omega). V) ;
hence ( |.r.| <= 1 & u in Up ((Omega). V) implies r * u in Up ((Omega). V) ) by RUSUB_4:def 5; :: thesis: verum