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

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

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

assume x in { ||.(u . (t,s)).|| where t is VECTOR of X, s is VECTOR of Y : ( ||.t.|| <= 1 & ||.s.|| <= 1 ) } ; :: thesis: x in REAL
then ex t being VECTOR of X ex s being VECTOR of Y st
( x = ||.(u . (t,s)).|| & ||.t.|| <= 1 & ||.s.|| <= 1 ) ;
hence x in REAL ; :: thesis: verum

end;

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

end;

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