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

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

end;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 )

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

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