environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, NAT_1, REAL_1, FINSEQ_1, RELAT_1, FUNCT_1, TARSKI, XREAL_0, FINSEQ_2, CARD_1, XXREAL_0, SEQ_1, ARYTM_3, CARD_3, MATRIX_1, TREES_1, ZFMISC_1, INCSP_1, MATRIXC1, QC_LANG1, ORDINAL4, PRE_POLY, BINOP_2, FINSEQ_3, RVSUM_1, STRUCT_0, VECTSP_1, SUPINF_2, FVSUM_1, MATRIXR1, MATRPROB, FUNCT_7, MATRIX_0, ASYMPT_1, XCMPLX_0;
notations HIDDEN, TARSKI, SUBSET_1, XBOOLE_0, XXREAL_0, XREAL_0, XCMPLX_0, REAL_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, SEQ_1, ZFMISC_1, FUNCOP_1, BINOP_1, BINOP_2, FUNCT_2, NAT_1, RVSUM_1, FINSEQ_1, FINSEQ_2, FINSEQOP, NEWTON, STRUCT_0, MATRLIN, MATRIXR1, MATRIX_3, MATRIX_0, GROUP_1, FVSUM_1, RLVECT_1, VECTSP_1;
definitions TARSKI;
theorems FUNCT_1, SEQ_1, NAT_1, TARSKI, ZFMISC_1, MATRIX_3, XREAL_1, BINOP_2, FVSUM_1, VECTSP_1, RLVECT_1, MATRLIN, XBOOLE_0, FINSEQ_1, PROB_3, MATRIX_0, FINSEQ_2, FUNCOP_1, RFINSEQ, FINSEQ_3, RVSUM_1, MATRIXR1, ORDINAL1, XREAL_0, MATRIXC1, XXREAL_0, STRUCT_0, PRE_POLY, CARD_1;
schemes CLASSES1, FINSEQ_2, PARTFUN1, NAT_1, MATRIX_0;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_2, STRUCT_0, VECTSP_1, MATRIX_0, MATRLIN, VALUED_0, CARD_1, RVSUM_1, XREAL_0;
constructors HIDDEN, REAL_1, BINOP_2, NEWTON, FVSUM_1, MATRIX_3, MATRLIN, MATRIXR1, BINOP_1, RVSUM_1, RELSET_1, FINSEQ_2, FINSEQ_4, SEQ_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities FINSEQ_1, FINSEQ_2, RVSUM_1;
expansions TARSKI, FINSEQ_1;
Lm1:
for r being Real
for m being Matrix of REAL holds
( ( for i, j being Nat st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Nat st i in dom m & j in dom (m . i) holds
(m . i) . j >= r )
Lm2:
for r being Real
for m being Matrix of REAL holds
( ( for i, j being Nat st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Nat st i in dom m & j in dom (Line (m,i)) holds
(Line (m,i)) . j >= r )
Lm3:
for r being Real
for m being Matrix of REAL holds
( ( for i, j being Nat st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Nat st j in Seg (width m) & i in dom (Col (m,j)) holds
(Col (m,j)) . i >= r )
Lm4:
0 in REAL
by XREAL_0:def 1;
definition
let x,
y be
FinSequence of
REAL ;
let M be
Matrix of
REAL;
assume that A1:
len x = len M
and A2:
len y = width M
;
existence
ex b1 being Matrix of REAL st
( len b1 = len x & width b1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) )
uniqueness
for b1, b2 being Matrix of REAL st len b1 = len x & width b1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) & len b2 = len x & width b2 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) holds
b1 = b2
end;
reconsider jj = 1, zz = 0 as Element of REAL by XREAL_0:def 1;