environ
vocabularies HIDDEN, NUMBERS, NAT_1, FINSEQ_2, FINSEQ_1, SUBSET_1, FUNCT_1, COMPLEX1, REAL_1, VALUED_0, RELAT_1, TARSKI, CARD_1, ARYTM_1, ARYTM_3, RVSUM_1, SQUARE_1, CARD_3, XXREAL_0, XCMPLX_0, ZFMISC_1, VALUED_1, PCOMPS_1, STRUCT_0, METRIC_1, XBOOLE_0, RLTOPSP1, PRE_TOPC, RLVECT_1, FUNCSDOM, SETFAM_1, ALGSTR_0, FUNCT_2, MONOID_0, BINOP_2, FUNCOP_1, SUPINF_2, MCART_1, EUCLID, VALUED_2, JORDAN2C, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, SETFAM_1, XREAL_0, COMPLEX1, NAT_1, RELAT_1, FUNCT_1, VALUED_0, STRUCT_0, METRIC_1, FUNCT_2, BINOP_1, BINOP_2, FUNCOP_1, REAL_1, VALUED_1, FINSEQ_1, FINSEQ_2, FINSEQOP, SQUARE_1, RVSUM_1, VALUED_2, MONOID_0, PRE_TOPC, PCOMPS_1, TOPMETR, XXREAL_0, ALGSTR_0, RLVECT_1, FUNCSDOM, RLTOPSP1;
definitions FINSEQ_1, PCOMPS_1, MONOID_0, VALUED_2, CARD_1;
theorems ABSVALUE, BINOP_1, FINSEQ_1, FINSEQ_2, FINSEQOP, FUNCT_1, FUNCT_2, PCOMPS_1, RVSUM_1, SQUARE_1, TARSKI, XREAL_0, COMPLEX1, XREAL_1, XXREAL_0, FUNCOP_1, ORDINAL1, VALUED_1, RELAT_1, PRE_TOPC, TOPMETR, RSSPACE, RLVECT_1, ALGSTR_0, FUNCSDOM, PARTFUN1, RFUNCT_1, CARD_1;
schemes FUNCT_2, BINOP_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, FINSEQ_2, RVSUM_1, METRIC_1, PCOMPS_1, MONOID_0, VALUED_0, VALUED_1, STRUCT_0, TOPMETR, RLTOPSP1, CARD_1, SQUARE_1, ORDINAL1;
constructors HIDDEN, REAL_1, SQUARE_1, BINOP_2, COMPLEX1, FINSEQOP, PCOMPS_1, MONOID_0, TOPMETR, RLTOPSP1, FUNCSDOM, VALUED_2, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities FINSEQ_1, STRUCT_0, PCOMPS_1, SQUARE_1, FINSEQ_2, RVSUM_1, VALUED_1, FUNCSDOM, RLVECT_1;
expansions MONOID_0;
Lm1:
for f being real-valued FinSequence holds f is Element of REAL (len f)
Lm2:
for f being real-valued FinSequence holds sqr (abs f) = sqr f
definition
let n be
Nat;
existence
ex b1 being Function of [:(REAL n),(REAL n):],REAL st
for x, y being Element of REAL n holds b1 . (x,y) = |.(x - y).|
uniqueness
for b1, b2 being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b1 . (x,y) = |.(x - y).| ) & ( for x, y being Element of REAL n holds b2 . (x,y) = |.(x - y).| ) holds
b1 = b2
end;
definition
let n be
Nat;
existence
ex b1 being strict RLTopStruct st
( TopStruct(# the carrier of b1, the topology of b1 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = RealVectSpace (Seg n) )
uniqueness
for b1, b2 being strict RLTopStruct st TopStruct(# the carrier of b1, the topology of b1 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = RealVectSpace (Seg n) & TopStruct(# the carrier of b2, the topology of b2 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = RealVectSpace (Seg n) holds
b1 = b2
;
end;
Lm3:
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds
p1 + p2 = r1 + r2
Lm4:
for n being Nat
for p being Point of (TOP-REAL n)
for x being Real
for r being real-valued Function st p = r holds
x * p = x (#) r
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;