begin
Lm1:
for r being Real
for m being Matrix of REAL holds
( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of 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 Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of 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 Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of NAT st j in Seg (width m) & i in dom (Col (m,j)) holds
(Col (m,j)) . i >= r )
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;