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

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

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

assume 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;

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

end;

||.(0. X).|| = 0 ;
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