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 SQUARE_1:17, BHSP_1:1;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 by XREAL_0:def 1; :: thesis: verum

end;then ex t being VECTOR of X st

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

hence x in REAL by XREAL_0:def 1; :: 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