let V be RealLinearSpace; :: thesis: Up ((0). 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 ((0). V) holds
r * u in Up ((0). V)
let r be Real; :: thesis: ( |.r.| <= 1 & u in Up ((0). V) implies r * u in Up ((0). V) )
assume that
|.r.| <= 1 and
A1: u in Up ((0). V) ; :: thesis: r * u in Up ((0). V)
u in the carrier of ((0). V) by A1, RUSUB_4:def 5;
then u in {(0. V)} by RLSUB_1:def 3;
then u = 0. V by TARSKI:def 1;
then r * u = 0. V ;
then r * u in {(0. V)} by TARSKI:def 1;
then r * u in the carrier of ((0). V) by RLSUB_1:def 3;
hence r * u in Up ((0). V) by RUSUB_4:def 5; :: thesis: verum