let n be non zero Nat; :: thesis: for x, y being Element of REAL n ex S being ext-real-membered set st
( S = { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } & (Infty_dist n) . (x,y) = sup S )
let x, y be Element of REAL n; :: thesis: ex S being ext-real-membered set st
( S = { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } & (Infty_dist n) . (x,y) = sup S )
set S = { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } ;
A1: ( { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } is real-membered & { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } = rng (abs (x - y)) ) by Th56;
then reconsider S1 = { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } as ext-real-membered set ;
take S1 ; :: thesis: ( S1 = { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } & (Infty_dist n) . (x,y) = sup S1 )
thus ( S1 = { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } & (Infty_dist n) . (x,y) = sup S1 ) by A1, Def7; :: thesis: verum