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

let x be object ; :: thesis: ( x in { ||.(u . t).|| where t is VECTOR of (product X) : for i being Element of dom X holds ||.(t . i).|| <= 1 } implies x in REAL )

now :: thesis: ( x in { ||.(u . t).|| where t is VECTOR of (product X) : for i being Element of dom X holds ||.(t . i).|| <= 1 } implies x in REAL )

assume x in { ||.(u . t).|| where t is VECTOR of (product X) : for i being Element of dom X holds ||.(t . i).|| <= 1 } ; :: thesis: x in REAL
then ex t being VECTOR of (product X) st
( x = ||.(u . t).|| & ( for i being Element of dom X holds ||.(t . i).|| <= 1 ) ) ;
hence x in REAL ; :: thesis: verum

end;

hence ( x in { ||.(u . t).|| where t is VECTOR of (product X) : for i being Element of dom X holds ||.(t . i).|| <= 1 } implies x in REAL ) ; :: thesis: verum

end;

A2: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
A3: dom X = dom (carr X) by LemmaX;
set x = 0. (product X);
reconsider s = 0. (product X) as Element of product (carr X) by A2;
for i being Element of dom X holds ||.((0. (product X)) . i).|| <= 1

proof

let i be Element of dom X; :: thesis: ||.((0. (product X)) . i).|| <= 1
s . i = 0. (X . i) by A2, A3, PRVECT_1:def 14;
hence ||.((0. (product X)) . i).|| <= 1 ; :: thesis: verum

end;

then ||.(u . (0. (product X))).|| in { ||.(u . t).|| where t is VECTOR of (product X) : for i being Element of dom X holds ||.(t . i).|| <= 1 } ;
hence { ||.(u . t).|| where t is VECTOR of (product X) : for i being Element of dom X holds ||.(t . i).|| <= 1 } is non empty Subset of REAL by A1, TARSKI:def 3; :: thesis: verum