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