environ
vocabularies HIDDEN, ALGSTR_0, ARYTM_1, ARYTM_3, CARD_1, CARD_3, CLASSES1, ENTROPY1, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FUNCT_1, FUNCT_2, FVSUM_1, INCSP_1, LMOD_7, MATRIX_1, MATRIX_3, MATRIX13, MATRLIN, MATRLIN2, MESFUNC1, NAT_1, NUMBERS, ORDINAL4, PARTFUN1, PBOOLE, PRE_TOPC, PRVECT_1, QC_LANG1, RANKNULL, RELAT_1, RLAFFIN1, RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_5, RVSUM_1, SEMI_AF1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, TREES_1, VALUED_0, VALUED_1, VECTSP_1, VECTSP10, XBOOLE_0, XXREAL_0, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, FINSET_1, FUNCT_1, RELSET_1, PARTFUN1, NAT_1, VALUED_0, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, STRUCT_0, RLVECT_1, RLVECT_2, RLVECT_3, VECTSP_1, MATRIX_0, MATRIX_1, MATRIX_3, VECTSP_4, VECTSP_6, VECTSP_7, MATRIX13, RVSUM_1, ALGSTR_0, FVSUM_1, RANKNULL, PRE_TOPC, MATRIX_6, MATRLIN, MATRLIN2, NAT_D, EUCLID, GROUP_1, MATRIX11, FINSEQOP, ENTROPY1, RLSUB_1, RUSUB_4, PRVECT_1, RLAFFIN1, MATRTOP1;
definitions TARSKI, XBOOLE_0;
theorems CARD_1, CARD_2, ENTROPY1, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_6, FUNCT_1, FUNCT_2, FVSUM_1, LAPLACE, MATRIX_0, MATRIX_6, MATRIX13, MATRIXR1, MATRLIN, MATRLIN2, MATRPROB, MATRTOP1, NAT_1, ORDINAL1, PARTFUN1, PRE_POLY, RANKNULL, RELAT_1, RLAFFIN1, RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_5, RVSUM_1, STRUCT_0, SUBSET_1, TARSKI, VECTSP_1, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, XBOOLE_0, XBOOLE_1, XREAL_0, XREAL_1, ZFMISC_1, TOPREAL3;
schemes FINSEQ_1, FUNCT_2, NAT_1;
registrations CARD_1, EUCLID, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_1, FUNCT_2, MATRIX13, MATRLIN2, MATRTOP1, MEMBERED, MONOID_0, NAT_1, NUMBERS, PRVECT_1, RELAT_1, RELSET_1, RLAFFIN1, RLVECT_3, RVSUM_1, STRUCT_0, RLVECT_2, VALUED_0, VECTSP_1, VECTSP_9, XREAL_0, XXREAL_0, MATRIX_6, ORDINAL1;
constructors HIDDEN, BINARITH, ENTROPY1, FVSUM_1, LAPLACE, MATRIX_6, MATRIX11, MATRIX13, MATRLIN2, MATRTOP1, MONOID_0, RANKNULL, REALSET1, RELSET_1, RLAFFIN1, RLVECT_3, RUSUB_5, VECTSP10, MATRIX15, MATRIX_1, MATRIX_4, FUNCSDOM, PCOMPS_1, SQUARE_1, BINOP_2;
requirements HIDDEN, ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
equalities EUCLID, FINSEQ_1, MATRIX13, MATRTOP1, STRUCT_0, VECTSP_1, XBOOLE_0;
expansions FINSEQ_1, STRUCT_0, TARSKI, XBOOLE_0;
Lm1:
for n being Nat holds the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)
Lm2:
for n being Nat holds 0. (n -VectSp_over F_Real) = 0. (TOP-REAL n)
Lm3:
for n being Nat
for f being b1 -element real-valued FinSequence holds f is Point of (TOP-REAL n)
Lm4:
for n, m being Nat
for M being Matrix of n,m,F_Real holds lines M c= [#] (Lin (lines M))
Lm5:
for n, m being Nat
for f being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real st card (lines M) = 1 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in Seg n holds
( L . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f ) ) )