let r be Real; :: thesis: 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 )
let m be Matrix of REAL; :: thesis: ( ( 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 )
hereby :: thesis: ( ( for i, j being Nat st i in dom m & j in dom (Line (m,i)) holds
(Line (m,i)) . j >= r ) implies for i, j being Nat st [i,j] in Indices m holds
m * (i,j) >= r )
assume A1: for i, j being Nat st [i,j] in Indices m holds
m * (i,j) >= r ; :: thesis: for i, j being Nat st i in dom m & j in dom (Line (m,i)) holds
(Line (m,i)) . j >= r
hereby :: thesis: verum
let i, j be Nat; :: thesis: ( i in dom m & j in dom (Line (m,i)) implies (Line (m,i)) . j >= r )
assume that
A2: i in dom m and
A3: j in dom (Line (m,i)) ; :: thesis: (Line (m,i)) . j >= r
m . i = Line (m,i) by A2, MATRIX_0:60;
hence (Line (m,i)) . j >= r by A1, A2, A3, Lm1; :: thesis: verum
end;
end;
assume A4: for i, j being Nat st i in dom m & j in dom (Line (m,i)) holds
(Line (m,i)) . j >= r ; :: thesis: for i, j being Nat st [i,j] in Indices m holds
m * (i,j) >= r
now :: thesis: for i being Nat st i in dom m holds
for j being Nat st j in dom (m . i) holds
(m . i) . j >= r
let i be Nat; :: thesis: ( i in dom m implies for j being Nat st j in dom (m . i) holds
(m . i) . j >= r )
assume A5: i in dom m ; :: thesis: for j being Nat st j in dom (m . i) holds
(m . i) . j >= r
m . i = Line (m,i) by A5, MATRIX_0:60;
hence for j being Nat st j in dom (m . i) holds
(m . i) . j >= r by A4, A5; :: thesis: verum
end;
then for i, j being Nat st i in dom m & j in dom (m . i) holds
(m . i) . j >= r ;
hence for i, j being Nat st [i,j] in Indices m holds
m * (i,j) >= r by Lm1; :: thesis: verum