environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, METRIC_1, CONVEX1, SUBSET_1, REAL_1, CARD_1, XXREAL_0, RELAT_1, ARYTM_1, FINSEQ_1, STRUCT_0, PARTFUN1, ARYTM_3, COMPLEX1, CARD_3, ZFMISC_1, BINTREE1, TREES_2, FUNCT_1, TREES_4, ORDINAL4, CAT_1, TREES_1, POWER, INT_1, NAT_1, FINSEQ_2, MARGREL1, EUCLID, XBOOLEAN, MCART_1, BINTREE2, ABIAN, TARSKI, RELAT_2, FUNCT_2, RLVECT_1, ALGSTR_0, BINOP_1, UNIALG_1, SUPINF_2, PRE_TOPC, GROUP_1, GROUP_2, VECTMETR, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, MCART_1, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, RELAT_2, XXREAL_0, INT_1, NAT_1, NAT_D, POWER, ABIAN, SERIES_1, RELAT_1, RELSET_1, MARGREL1, BINOP_1, DOMAIN_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0, ALGSTR_0, PRE_TOPC, FINSEQ_1, FINSEQ_2, FINSEQ_4, BINARITH, TREES_1, TREES_2, TREES_4, BINTREE1, BINTREE2, RVSUM_1, RLVECT_1, GROUP_1, GROUP_2, TOPS_2, METRIC_1, EUCLID;
definitions FUNCT_2, STRUCT_0, TARSKI, XBOOLE_0, ALGSTR_0;
theorems TARSKI, MCART_1, NAT_1, NAT_2, ZFMISC_1, BINOP_1, RELAT_1, FUNCT_1, FUNCT_2, POWER, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_5, BINARI_2, BINARI_3, ABSVALUE, TOPS_2, FUNCOP_1, BINTREE2, PRE_FF, RLVECT_1, METRIC_1, RVSUM_1, EUCLID, GROUP_1, GROUP_2, RELAT_2, XCMPLX_1, PARTFUN1, INT_1, ORDERS_1, XREAL_1, FINSEQOP, XXREAL_0, FINSOP_1, NAT_D, ORDINAL1, XREAL_0, XTUPLE_0;
schemes BINOP_1, NAT_1, FINSEQ_2, BINTREE2, RELSET_1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, NAT_1, FINSEQ_1, BINOP_2, MARGREL1, FINSEQ_2, TREES_2, STRUCT_0, METRIC_1, GROUP_2, BINTREE1, BINTREE2, VALUED_0, XREAL_0, RELAT_1, INT_1, EUCLID, ORDINAL1, CARD_1, XTUPLE_0;
constructors HIDDEN, REAL_1, NAT_D, FINSEQOP, FINSEQ_4, FINSOP_1, SERIES_1, REALSET1, BINARITH, ABIAN, TOPS_2, GROUP_2, EUCLID, BINTREE2, RVSUM_1, RELSET_1, XTUPLE_0, BINOP_1, BINOP_2, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0, MARGREL1, XBOOLEAN, RLVECT_1, RVSUM_1, EUCLID, FINSEQ_2, ALGSTR_0, VALUED_1;
expansions STRUCT_0, TARSKI, RLVECT_1;
definition
let n be
Element of
NAT ;
existence
ex b1 being strict RealLinearMetrSpace st
( the carrier of b1 = REAL n & the distance of b1 = Pitag_dist n & 0. b1 = 0* n & ( for x, y being Element of REAL n holds the addF of b1 . (x,y) = x + y ) & ( for x being Element of REAL n
for r being Element of REAL holds the Mult of b1 . (r,x) = r * x ) )
uniqueness
for b1, b2 being strict RealLinearMetrSpace st the carrier of b1 = REAL n & the distance of b1 = Pitag_dist n & 0. b1 = 0* n & ( for x, y being Element of REAL n holds the addF of b1 . (x,y) = x + y ) & ( for x being Element of REAL n
for r being Element of REAL holds the Mult of b1 . (r,x) = r * x ) & the carrier of b2 = REAL n & the distance of b2 = Pitag_dist n & 0. b2 = 0* n & ( for x, y being Element of REAL n holds the addF of b2 . (x,y) = x + y ) & ( for x being Element of REAL n
for r being Element of REAL holds the Mult of b2 . (r,x) = r * x ) holds
b1 = b2
end;