A1: now :: thesis: for x being object st x in { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } holds

x in REAL

||.(0. X).|| = 0
by CLVECT_1:102;x in REAL

let x be object ; :: thesis: ( x in { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } implies x in REAL )

end;now :: thesis: ( x in { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } implies x in REAL )

hence
( x in { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } implies x in REAL )
; :: thesis: verumassume
x in { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 }
; :: thesis: x in REAL

then ex t being VECTOR of X st

( x = ||.(u . t).|| & ||.t.|| <= 1 ) ;

hence x in REAL ; :: thesis: verum

end;then ex t being VECTOR of X st

( x = ||.(u . t).|| & ||.t.|| <= 1 ) ;

hence x in REAL ; :: thesis: verum

then ||.(u . (0. X)).|| in { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } ;

hence { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } is non empty Subset of REAL by A1, TARSKI:def 3; :: thesis: verum