consider K being Real such that

A1: 0 <= K and

A2: for x being VECTOR of X

for y being VECTOR of Y holds ||.(g . (x,y)).|| <= (K * ||.x.||) * ||.y.|| by Def8;

take K ; :: according to XXREAL_2:def 10 :: thesis: K is UpperBound of PreNorms g

let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in PreNorms g or r <= K )

assume r in PreNorms g ; :: thesis: r <= K

then consider t being VECTOR of X, s being VECTOR of Y such that

A3: r = ||.(g . (t,s)).|| and

A4: ( ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

A5: ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.|| by A2;

||.t.|| * ||.s.|| <= 1 * 1 by XREAL_1:66, A4;

then K * (||.t.|| * ||.s.||) <= K * 1 by A1, XREAL_1:64;

hence r <= K by A3, A5, XXREAL_0:2; :: thesis: verum

A1: 0 <= K and

A2: for x being VECTOR of X

for y being VECTOR of Y holds ||.(g . (x,y)).|| <= (K * ||.x.||) * ||.y.|| by Def8;

take K ; :: according to XXREAL_2:def 10 :: thesis: K is UpperBound of PreNorms g

let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in PreNorms g or r <= K )

assume r in PreNorms g ; :: thesis: r <= K

then consider t being VECTOR of X, s being VECTOR of Y such that

A3: r = ||.(g . (t,s)).|| and

A4: ( ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

A5: ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.|| by A2;

||.t.|| * ||.s.|| <= 1 * 1 by XREAL_1:66, A4;

then K * (||.t.|| * ||.s.||) <= K * 1 by A1, XREAL_1:64;

hence r <= K by A3, A5, XXREAL_0:2; :: thesis: verum