1. The Real Euclidean Space as a Real Linear Space

In this paper n is a natural number. Let n be a natural number. The functor ?E n, ? · ? ? yields a strict non empty normed structure and is defined by the conditions (Def. 1). (Def. 1)(i) The carrier of ?E n, ? · ? ? = R n, (ii) the zero of ?En, ? · ? ?

FORMALIZED

Volume

UniversityofMATHEMATICSBia lystok,200513,Number4,Pages577–580

CompletenessoftheRealEuclideanSpace

NoboruEndou

GifuNationalCollegeofTechnology

Gifu,JapanYasunariShidamaShinshuUniversityNagano,Japan

MMLidenti er:REALNS1,version:7.6.014.50.934

Theterminologyandnotationusedhereareintroducedinthefollowingarticles:

[21],[8],[24],[25],[6],[26],[7],[3],[14],[2],[5],[1],[20],[22],[4],[23],[15],[16],

[13],[12],[11],[9],[18],[10],[19],and[17].

1.TheRealEuclideanSpaceasaRealLinearSpace

Inthispapernisanaturalnumber.

Letnbeanaturalnumber.Thefunctor En, · yieldsastrictnonempty

normedstructureandisde nedbytheconditions(Def.1).

(Def.1)(i)Thecarrierof En, · =Rn,

(ii)thezeroof En, · = 0,...,0 , Rnn

(iii)forallelementsa,bofholds(theadditionof En, · )(a,b)=a+b,(iv)foreveryelementrofRandforeveryelementxofRnholds(the

externalmultiplicationof En, · )(r,x)=r·x,and

(v)foreveryelementxofRnholds(thenormof En, · )(x)=|x|.

Letnbeanaturalnumber.Notethattheadditionof En, · iscommu-

tativeandassociative.

Letnbeanonemptynaturalnumber.Notethat En, · isnontrivial.

Onecanprovethefollowingpropositions:

(1)Foreveryvectorxof En, · andforeveryelementyofRnsuchthat

x=yholds x =|y|.

(2)Letnbeanaturalnumber,x,ybevectorsof En, · ,anda,bbe

elementsofRn.Ifx=aandy=b,thenx+y=a+b.

577c 2005UniversityofBia lystok

ISSN1426–2630