environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, SEQ_1, NAT_1, EUCLID, REAL_1, PRE_TOPC, FUNCT_1, RELAT_1, VALUED_0, TARSKI, STRUCT_0, SUPINF_2, ARYTM_3, ARYTM_1, COMPLEX1, VALUED_1, CARD_1, XXREAL_0, XXREAL_2, SEQ_2, ORDINAL2, XBOOLE_0, PARTFUN1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, VALUED_1, PARTFUN1, COMPLEX1, REAL_1, PRE_TOPC, XXREAL_0, XCMPLX_0, XREAL_0, NAT_1, SEQ_1, STRUCT_0, RLVECT_1, VFUNCT_1, EUCLID;
definitions FUNCT_2;
theorems FUNCT_1, FUNCT_2, TARSKI, EUCLID, SEQ_1, NAT_1, XBOOLE_0, NORMSP_1, XCMPLX_0, XREAL_1, COMPLEX1, XXREAL_0, VFUNCT_1, ORDINAL1, RLVECT_1;
schemes SEQ_1, NAT_1;
registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, MONOID_0, EUCLID, XBOOLE_0, VALUED_1, FUNCT_2, NUMBERS, VALUED_0, NAT_1;
constructors HIDDEN, REAL_1, COMPLEX1, MONOID_0, EUCLID, RELSET_1, BINOP_2, VFUNCT_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities STRUCT_0, RLVECT_1;
expansions ;
theorem Th10:
for
N being
Nat for
seq1,
seq2,
seq3 being
Real_Sequence of
N holds
(seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
theorem
for
N being
Nat for
seq1,
seq2,
seq3 being
Real_Sequence of
N holds
seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
theorem
for
N being
Nat for
seq1,
seq2,
seq3 being
Real_Sequence of
N holds
seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
Lm1:
for N being Nat
for w1, w2 being Point of (TOP-REAL N) st |.(w1 - w2).| = 0 holds
w1 = w2
Lm2:
for N being Nat
for w1, w2 being Point of (TOP-REAL N) st w1 = w2 holds
|.(w1 - w2).| = 0