:: MATRIX10 semantic presentation

begin


definition
let M be Matrix of REAL;
attrM is Positive  means :Def1: :: MATRIX10:def 1
 for i, j being Nat st [i,j] in Indices M holds
M * (i,j) > 0 ;
attrM is Negative  means :Def2: :: MATRIX10:def 2
 for i, j being Nat st [i,j] in Indices M holds
M * (i,j) < 0 ;
attrM is Nonpositive  means :Def3: :: MATRIX10:def 3
 for i, j being Nat st [i,j] in Indices M holds
M * (i,j) <= 0 ;
attrM is Nonnegative  means :Def4: :: MATRIX10:def 4
 for i, j being Nat st [i,j] in Indices M holds
M * (i,j) >= 0 ;
end;

:: deftheorem Def1 defines Positive MATRIX10:def_1_:_
 for M being Matrix of REAL holds
( M is Positive iff for i, j being Nat st [i,j] in Indices M holds
M * (i,j) > 0 );

:: deftheorem Def2 defines Negative MATRIX10:def_2_:_
 for M being Matrix of REAL holds
( M is Negative iff for i, j being Nat st [i,j] in Indices M holds
M * (i,j) < 0 );

:: deftheorem Def3 defines Nonpositive MATRIX10:def_3_:_
 for M being Matrix of REAL holds
( M is Nonpositive iff for i, j being Nat st [i,j] in Indices M holds
M * (i,j) <= 0 );

:: deftheorem Def4 defines Nonnegative MATRIX10:def_4_:_
 for M being Matrix of REAL holds
( M is Nonnegative iff for i, j being Nat st [i,j] in Indices M holds
M * (i,j) >= 0 );

definition
let M1, M2 be Matrix of REAL;
predM1 is_less_than M2 means :Def5: :: MATRIX10:def 5
 for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) < M2 * (i,j);
predM1 is_less_or_equal_with M2 means :Def6: :: MATRIX10:def 6
 for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) <= M2 * (i,j);
end;

:: deftheorem Def5 defines is_less_than MATRIX10:def_5_:_
 for M1, M2 being Matrix of REAL holds
( M1 is_less_than M2 iff for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) < M2 * (i,j) );

:: deftheorem Def6 defines is_less_or_equal_with MATRIX10:def_6_:_
 for M1, M2 being Matrix of REAL holds
( M1 is_less_or_equal_with M2 iff for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) <= M2 * (i,j) );

definition
let M be Matrix of REAL;
func|:M:| ->  Matrix of REAL means :Def7: :: MATRIX10:def 7
( len it = len M & width it = width M & ( for i, j being Nat st [i,j] in Indices M holds
it * (i,j) = abs (M * (i,j)) ) );
existence
 ex b1 being Matrix of REAL st
( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = abs (M * (i,j)) ) )
proof
deffunc H1( Nat, Nat) ->  Element of REAL = abs (M * ($1,$2));
consider M1 being Matrix of len M, width M, REAL  such that
A1: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = H1(i,j) from MATRIX_1:sch_1();
take  M1 ; ::_thesis: ( len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = abs (M * (i,j)) ) )
A2: len M1 = len M by MATRIX_1:def_2;
A3: now__::_thesis:_(_(_len_M_=_0_&_width_M1_=_width_M_)_or_(_len_M_>_0_&_width_M1_=_width_M_)_)
percases ( len M = 0 or len M > 0 ) ;
caseA4: len M = 0 ; ::_thesis: width M1 = width M
then  width M1 = 0 by A2, MATRIX_1:def_3;
hence  width M1 = width M by A4, MATRIX_1:def_3; ::_thesis: verum
end;
case len M > 0 ; ::_thesis: width M1 = width M
hence  width M1 = width M by MATRIX_1:23; ::_thesis: verum
end;
end;
end;
 dom M = dom M1 by A2, FINSEQ_3:29;
hence  ( len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = abs (M * (i,j)) ) ) by A1, A3, MATRIX_1:def_2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Matrix of REAL st len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = abs (M * (i,j)) ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = abs (M * (i,j)) ) holds
b1 = b2
proof
let M1, M2 be Matrix of REAL; ::_thesis: ( len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = abs (M * (i,j)) ) & len M2 = len M & width M2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
M2 * (i,j) = abs (M * (i,j)) ) implies M1 = M2 )
assume that
A5: len M1 = len M and
A6: width M1 = width M and
A7: for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = abs (M * (i,j)) and
A8: ( len M2 = len M & width M2 = width M ) and
A9: for i, j being Nat st [i,j] in Indices M holds
M2 * (i,j) = abs (M * (i,j)) ; ::_thesis: M1 = M2
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_M1_holds_
M1_*_(i,j)_=_M2_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A10: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
A11: dom M1 = dom M by A5, FINSEQ_3:29;
hence M1 * (i,j) = abs (M * (i,j)) by A6, A7, A10
.= M2 * (i,j) by A6, A9, A10, A11 ;
::_thesis: verum
end;
hence  M1 = M2 by A5, A6, A8, MATRIX_1:21; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines |: MATRIX10:def_7_:_
 for M, b2 being Matrix of REAL holds
( b2 = |:M:| iff ( len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = abs (M * (i,j)) ) ) );

definition
let n be Nat;
let M be Matrix of n, REAL ;
:: original: -
redefine func - M ->  Matrix of n, REAL ;
coherence
 - M is Matrix of n, REAL
proof
 len M = n by MATRIX_1:24;
then A1: len (- M) = n by MATRIX_3:def_2;
 width M = n by MATRIX_1:24;
then  width (- M) = n by MATRIX_3:def_2;
hence  - M is Matrix of n, REAL by A1, MATRIX_2:7; ::_thesis: verum
end;
end;

definition
let n be Nat;
let M1, M2 be Matrix of n, REAL ;
:: original: +
redefine funcM1 + M2 ->  Matrix of n, REAL ;
coherence
 M1 + M2 is Matrix of n, REAL
proof
A1: width M2 = n by MATRIX_1:24;
 width M1 = n by MATRIX_1:24;
then  ( len (M1 + M2) = len M1 & width (M1 + M2) = width M2 ) by A1, MATRIX_3:def_3;
hence  M1 + M2 is Matrix of n, REAL by A1, MATRIX_1:24, MATRIX_2:7; ::_thesis: verum
end;
end;

definition
let n be Nat;
let M1, M2 be Matrix of n, REAL ;
:: original: -
redefine funcM1 - M2 ->  Matrix of n, REAL ;
coherence
 M1 - M2 is Matrix of n, REAL
proof
 len (M1 + (- M2)) = len M1 by MATRIX_3:def_3;
hence  M1 - M2 is Matrix of n, REAL by MATRIX_4:def_1; ::_thesis: verum
end;
end;

definition
let n be Nat;
let a be Element of REAL ;
let M be Matrix of n, REAL ;
:: original: *
redefine funca * M ->  Matrix of n, REAL ;
coherence
 a * M is Matrix of n, REAL
proof
A1: width (a * M) = width M by MATRIXR1:27;
 ( width M = n & len (a * M) = len M ) by MATRIXR1:27, MATRIX_1:24;
hence  a * M is Matrix of n, REAL by A1, MATRIX_1:24, MATRIX_2:7; ::_thesis: verum
end;
end;

registration
cluster(1,1) --> 1 ->  Positive for Matrix of REAL;
coherence
 for b1 being Matrix of REAL st b1 = (1,1) --> 1 holds
b1 is Positive
proof
 for i, j being Nat st [i,j] in Indices ((1,1) --> 1) holds
((1,1) --> 1) * (i,j) > 0 by MATRIX_2:1;
hence  for b1 being Matrix of REAL st b1 = (1,1) --> 1 holds
b1 is Positive by Def1; ::_thesis: verum
end;
cluster(1,1) --> 1 ->  Nonnegative for Matrix of REAL;
coherence
 for b1 being Matrix of REAL st b1 = (1,1) --> 1 holds
b1 is Nonnegative
proof
 for i, j being Nat st [i,j] in Indices ((1,1) --> 1) holds
((1,1) --> 1) * (i,j) >= 0 by MATRIX_2:1;
hence  for b1 being Matrix of REAL st b1 = (1,1) --> 1 holds
b1 is Nonnegative by Def4; ::_thesis: verum
end;
cluster(1,1) --> (- 1) ->  Negative for Matrix of REAL;
coherence
 for b1 being Matrix of REAL st b1 = (1,1) --> (- 1) holds
b1 is Negative
proof
 for i, j being Nat st [i,j] in Indices ((1,1) --> (- 1)) holds
((1,1) --> (- 1)) * (i,j) < 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((1,1) --> (- 1)) implies ((1,1) --> (- 1)) * (i,j) < 0 )
assume  [i,j] in Indices ((1,1) --> (- 1)) ; ::_thesis: ((1,1) --> (- 1)) * (i,j) < 0
then  ((1,1) --> (- 1)) * (i,j) = - 1 by MATRIX_2:1;
hence  ((1,1) --> (- 1)) * (i,j) < 0 ; ::_thesis: verum
end;
hence  for b1 being Matrix of REAL st b1 = (1,1) --> (- 1) holds
b1 is Negative by Def2; ::_thesis: verum
end;
cluster(1,1) --> (- 1) ->  Nonpositive for Matrix of REAL;
coherence
 for b1 being Matrix of REAL st b1 = (1,1) --> (- 1) holds
b1 is Nonpositive
proof
 for i, j being Nat st [i,j] in Indices ((1,1) --> (- 1)) holds
((1,1) --> (- 1)) * (i,j) <= 0 by MATRIX_2:1;
hence  for b1 being Matrix of REAL st b1 = (1,1) --> (- 1) holds
b1 is Nonpositive by Def3; ::_thesis: verum
end;
end;

registration
clusterV16() V19( NAT ) V20(K291(REAL)) V21() FinSequence-like tabular Positive Nonnegative for FinSequence of K291(REAL);
existence
 ex b1 being Matrix of REAL st
( b1 is Positive & b1 is Nonnegative )
proof
take  (1,1) --> 1 ; ::_thesis: ( (1,1) --> 1 is Positive & (1,1) --> 1 is Nonnegative )
thus  ( (1,1) --> 1 is Positive & (1,1) --> 1 is Nonnegative ) ; ::_thesis: verum
end;
clusterV16() V19( NAT ) V20(K291(REAL)) V21() FinSequence-like tabular Negative Nonpositive for FinSequence of K291(REAL);
existence
 ex b1 being Matrix of REAL st
( b1 is Negative & b1 is Nonpositive )
proof
take  (1,1) --> (- 1) ; ::_thesis: ( (1,1) --> (- 1) is Negative & (1,1) --> (- 1) is Nonpositive )
thus  ( (1,1) --> (- 1) is Negative & (1,1) --> (- 1) is Nonpositive ) ; ::_thesis: verum
end;
end;

registration
let M be Positive Matrix of REAL;
clusterM @  ->  Positive ;
coherence
 M @ is Positive
proof
 for i, j being Nat st [i,j] in Indices (M @) holds
(M @) * (i,j) > 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M @) implies (M @) * (i,j) > 0 )
assume  [i,j] in Indices (M @) ; ::_thesis: (M @) * (i,j) > 0
then A1: [j,i] in Indices M by MATRIX_1:def_6;
then  (M @) * (i,j) = M * (j,i) by MATRIX_1:def_6;
hence  (M @) * (i,j) > 0 by A1, Def1; ::_thesis: verum
end;
hence  M @ is Positive by Def1; ::_thesis: verum
end;
end;

registration
let M be Negative Matrix of REAL;
clusterM @  ->  Negative ;
coherence
 M @ is Negative
proof
 for i, j being Nat st [i,j] in Indices (M @) holds
(M @) * (i,j) < 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M @) implies (M @) * (i,j) < 0 )
assume  [i,j] in Indices (M @) ; ::_thesis: (M @) * (i,j) < 0
then A1: [j,i] in Indices M by MATRIX_1:def_6;
then  (M @) * (i,j) = M * (j,i) by MATRIX_1:def_6;
hence  (M @) * (i,j) < 0 by A1, Def2; ::_thesis: verum
end;
hence  M @ is Negative by Def2; ::_thesis: verum
end;
end;

registration
let M be Nonpositive Matrix of REAL;
clusterM @  ->  Nonpositive ;
coherence
 M @ is Nonpositive
proof
 for i, j being Nat st [i,j] in Indices (M @) holds
(M @) * (i,j) <= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M @) implies (M @) * (i,j) <= 0 )
assume  [i,j] in Indices (M @) ; ::_thesis: (M @) * (i,j) <= 0
then A1: [j,i] in Indices M by MATRIX_1:def_6;
then  (M @) * (i,j) = M * (j,i) by MATRIX_1:def_6;
hence  (M @) * (i,j) <= 0 by A1, Def3; ::_thesis: verum
end;
hence  M @ is Nonpositive by Def3; ::_thesis: verum
end;
end;

registration
let M be Nonnegative Matrix of REAL;
clusterM @  ->  Nonnegative ;
coherence
 M @ is Nonnegative
proof
 for i, j being Nat st [i,j] in Indices (M @) holds
(M @) * (i,j) >= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M @) implies (M @) * (i,j) >= 0 )
assume  [i,j] in Indices (M @) ; ::_thesis: (M @) * (i,j) >= 0
then A1: [j,i] in Indices M by MATRIX_1:def_6;
then  (M @) * (i,j) = M * (j,i) by MATRIX_1:def_6;
hence  (M @) * (i,j) >= 0 by A1, Def4; ::_thesis: verum
end;
hence  M @ is Nonnegative by Def4; ::_thesis: verum
end;
end;

registration
let n be Nat;
cluster(n,n) --> 1 ->  Positive for Matrix of n, REAL ;
coherence
 for b1 being Matrix of n, REAL st b1 = (n,n) --> 1 holds
b1 is Positive
proof
 for i, j being Nat st [i,j] in Indices ((n,n) --> 1) holds
((n,n) --> 1) * (i,j) > 0 by MATRIX_2:1;
hence  for b1 being Matrix of n, REAL st b1 = (n,n) --> 1 holds
b1 is Positive by Def1; ::_thesis: verum
end;
cluster(n,n) --> (- 1) ->  Negative for Matrix of n, REAL ;
coherence
 for b1 being Matrix of n, REAL st b1 = (n,n) --> (- 1) holds
b1 is Negative
proof
 for i, j being Nat st [i,j] in Indices ((n,n) --> (- 1)) holds
((n,n) --> (- 1)) * (i,j) < 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((n,n) --> (- 1)) implies ((n,n) --> (- 1)) * (i,j) < 0 )
assume  [i,j] in Indices ((n,n) --> (- 1)) ; ::_thesis: ((n,n) --> (- 1)) * (i,j) < 0
then  ((n,n) --> (- 1)) * (i,j) = - 1 by MATRIX_2:1;
hence  ((n,n) --> (- 1)) * (i,j) < 0 ; ::_thesis: verum
end;
hence  for b1 being Matrix of n, REAL st b1 = (n,n) --> (- 1) holds
b1 is Negative by Def2; ::_thesis: verum
end;
cluster(n,n) --> (- 1) ->  Nonpositive for Matrix of n, REAL ;
coherence
 for b1 being Matrix of n, REAL st b1 = (n,n) --> (- 1) holds
b1 is Nonpositive
proof
 for i, j being Nat st [i,j] in Indices ((n,n) --> (- 1)) holds
((n,n) --> (- 1)) * (i,j) <= 0 by MATRIX_2:1;
hence  for b1 being Matrix of n, REAL st b1 = (n,n) --> (- 1) holds
b1 is Nonpositive by Def3; ::_thesis: verum
end;
cluster(n,n) --> 1 ->  Nonnegative for Matrix of n, REAL ;
coherence
 for b1 being Matrix of n, REAL st b1 = (n,n) --> 1 holds
b1 is Nonnegative
proof
 for i, j being Nat st [i,j] in Indices ((n,n) --> 1) holds
((n,n) --> 1) * (i,j) >= 0 by MATRIX_2:1;
hence  for b1 being Matrix of n, REAL st b1 = (n,n) --> 1 holds
b1 is Nonnegative by Def4; ::_thesis: verum
end;
end;

registration
let n be Nat;
clusterV16() V19( NAT ) V20(K291(REAL)) V21() FinSequence-like tabular Positive Nonnegative for Matrix of n,n, REAL ;
existence
 ex b1 being Matrix of n, REAL st
( b1 is Positive & b1 is Nonnegative )
proof
take  (n,n) --> 1 ; ::_thesis: ( (n,n) --> 1 is Positive & (n,n) --> 1 is Nonnegative )
thus  ( (n,n) --> 1 is Positive & (n,n) --> 1 is Nonnegative ) ; ::_thesis: verum
end;
clusterV16() V19( NAT ) V20(K291(REAL)) V21() FinSequence-like tabular Negative Nonpositive for Matrix of n,n, REAL ;
existence
 ex b1 being Matrix of n, REAL st
( b1 is Negative & b1 is Nonpositive )
proof
take  (n,n) --> (- 1) ; ::_thesis: ( (n,n) --> (- 1) is Negative & (n,n) --> (- 1) is Nonpositive )
thus  ( (n,n) --> (- 1) is Negative & (n,n) --> (- 1) is Nonpositive ) ; ::_thesis: verum
end;
end;

Lm1:  for n being Nat
for M1, M2 being Matrix of n, REAL holds
( len M1 = len M2 & width M1 = width M2 )
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL holds
( len M1 = len M2 & width M1 = width M2 )
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( len M1 = len M2 & width M1 = width M2 )
 ( width M1 = n & len M1 = n ) by MATRIX_1:24;
hence  ( len M1 = len M2 & width M1 = width M2 ) by MATRIX_1:24; ::_thesis: verum
end;

theorem :: MATRIX10:1
for x1 being Element of F_Real
for x2 being Real st x1 = x2 holds
- x1 = - x2 ;

theorem Th2: :: MATRIX10:2
for i, j being Nat
for M being Matrix of REAL st [i,j] in Indices M holds
(- M) * (i,j) = - (M * (i,j))
proof
let i, j be Nat; ::_thesis: for M being Matrix of REAL st [i,j] in Indices M holds
(- M) * (i,j) = - (M * (i,j))
let M be Matrix of REAL; ::_thesis: ( [i,j] in Indices M implies (- M) * (i,j) = - (M * (i,j)) )
assume  [i,j] in Indices M ; ::_thesis: (- M) * (i,j) = - (M * (i,j))
then  (- M) * (i,j) = - ((MXR2MXF M) * (i,j)) by MATRIX_3:def_2, VECTSP_1:def_5;
hence  (- M) * (i,j) = - (M * (i,j)) by VECTSP_1:def_5; ::_thesis: verum
end;

theorem Th3: :: MATRIX10:3
for i, j being Nat
for M1, M2 being Matrix of REAL st len M1 = len M2 & width M1 = width M2 & [i,j] in Indices M1 holds
(M1 - M2) * (i,j) = (M1 * (i,j)) - (M2 * (i,j))
proof
let i, j be Nat; ::_thesis: for M1, M2 being Matrix of REAL st len M1 = len M2 & width M1 = width M2 & [i,j] in Indices M1 holds
(M1 - M2) * (i,j) = (M1 * (i,j)) - (M2 * (i,j))
let M1, M2 be Matrix of REAL; ::_thesis: ( len M1 = len M2 & width M1 = width M2 & [i,j] in Indices M1 implies (M1 - M2) * (i,j) = (M1 * (i,j)) - (M2 * (i,j)) )
assume that
A1: len M1 = len M2 and
A2: width M1 = width M2 and
A3: [i,j] in Indices M1 ; ::_thesis: (M1 - M2) * (i,j) = (M1 * (i,j)) - (M2 * (i,j))
A4: ( 1 <= j & j <= width M2 ) by A2, A3, MATRIXC1:1;
 ( 1 <= i & i <= len M2 ) by A1, A3, MATRIXC1:1;
then A5: [i,j] in Indices (MXR2MXF M2) by A4, MATRIXC1:1;
(M1 - M2) * (i,j) = ((MXR2MXF M1) + (- (MXR2MXF M2))) * (i,j) by MATRIX_4:def_1, VECTSP_1:def_5
.= ((MXR2MXF M1) * (i,j)) + ((- (MXR2MXF M2)) * (i,j)) by A3, MATRIX_3:def_3
.= ((MXR2MXF M1) * (i,j)) + (- ((MXR2MXF M2) * (i,j))) by A5, MATRIX_3:def_2 ;
hence  (M1 - M2) * (i,j) = (M1 * (i,j)) - (M2 * (i,j)) by VECTSP_1:def_5; ::_thesis: verum
end;

theorem Th4: :: MATRIX10:4
for a being Element of REAL
for i, j being Nat
for M being Matrix of REAL st [i,j] in Indices M holds
(a * M) * (i,j) = a * (M * (i,j))
proof
let a be Element of REAL ; ::_thesis: for i, j being Nat
for M being Matrix of REAL st [i,j] in Indices M holds
(a * M) * (i,j) = a * (M * (i,j))
let i, j be Nat; ::_thesis: for M being Matrix of REAL st [i,j] in Indices M holds
(a * M) * (i,j) = a * (M * (i,j))
let M be Matrix of REAL; ::_thesis: ( [i,j] in Indices M implies (a * M) * (i,j) = a * (M * (i,j)) )
reconsider aa = a as Element of F_Real by VECTSP_1:def_5;
A1: MXR2MXF (a * M) = MXR2MXF (MXF2MXR (aa * (MXR2MXF M))) by MATRIXR1:def_7
.= aa * (MXR2MXF M) ;
assume  [i,j] in Indices M ; ::_thesis: (a * M) * (i,j) = a * (M * (i,j))
then  (a * M) * (i,j) = aa * ((MXR2MXF M) * (i,j)) by A1, MATRIX_3:def_5, VECTSP_1:def_5;
hence  (a * M) * (i,j) = a * (M * (i,j)) by VECTSP_1:def_5; ::_thesis: verum
end;

theorem Th5: :: MATRIX10:5
for n being Nat
for M being Matrix of n, REAL holds Indices M = Indices |:M:|
proof
let n be Nat; ::_thesis: for M being Matrix of n, REAL holds Indices M = Indices |:M:|
let M be Matrix of n, REAL ; ::_thesis: Indices M = Indices |:M:|
A1: Seg (len M) = dom M by FINSEQ_1:def_3;
 ( len |:M:| = len M & width |:M:| = width M ) by Def7;
hence  Indices M = Indices |:M:| by A1, FINSEQ_1:def_3; ::_thesis: verum
end;

theorem :: MATRIX10:6
for a being Element of REAL
for n being Nat
for M being Matrix of n, REAL holds |:(a * M):| = (abs a) * |:M:|
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M being Matrix of n, REAL holds |:(a * M):| = (abs a) * |:M:|
let n be Nat; ::_thesis: for M being Matrix of n, REAL holds |:(a * M):| = (abs a) * |:M:|
let M be Matrix of n, REAL ; ::_thesis: |:(a * M):| = (abs a) * |:M:|
A1: ( len (a * M) = len M & width (a * M) = width M ) by MATRIXR1:27;
 len ((abs a) * |:M:|) = len |:M:| by MATRIXR1:27;
then A2: len ((abs a) * |:M:|) = len M by Def7;
A3: for i, j being Nat st [i,j] in Indices |:(a * M):| holds
|:(a * M):| * (i,j) = ((abs a) * |:M:|) * (i,j)
proof
A4: Indices (a * M) = Indices M by MATRIXR1:28;
A5: Indices (a * M) = Indices M by MATRIXR1:28;
let i, j be Nat; ::_thesis: ( [i,j] in Indices |:(a * M):| implies |:(a * M):| * (i,j) = ((abs a) * |:M:|) * (i,j) )
assume A6: [i,j] in Indices |:(a * M):| ; ::_thesis: |:(a * M):| * (i,j) = ((abs a) * |:M:|) * (i,j)
A7: Indices |:(a * M):| = Indices (a * M) by Th5;
then A8: |:(a * M):| * (i,j) = abs ((a * M) * (i,j)) by A6, Def7
.= abs (a * (M * (i,j))) by A6, A7, A4, Th4
.= (abs a) * (abs (M * (i,j))) by COMPLEX1:65 ;
 Indices |:M:| = Indices M by Th5;
then ((abs a) * |:M:|) * (i,j) = (abs a) * (|:M:| * (i,j)) by A6, A7, A5, Th4
.= |:(a * M):| * (i,j) by A6, A7, A8, A5, Def7 ;
hence  |:(a * M):| * (i,j) = ((abs a) * |:M:|) * (i,j) ; ::_thesis: verum
end;
 width ((abs a) * |:M:|) = width |:M:| by MATRIXR1:27;
then A9: width ((abs a) * |:M:|) = width M by Def7;
 ( len |:(a * M):| = len (a * M) & width |:(a * M):| = width (a * M) ) by Def7;
hence  |:(a * M):| = (abs a) * |:M:| by A1, A2, A9, A3, MATRIX_1:21; ::_thesis: verum
end;

theorem :: MATRIX10:7
for n being Nat
for M being Matrix of n, REAL st M is Negative holds
- M is Positive
proof
let n be Nat; ::_thesis: for M being Matrix of n, REAL st M is Negative holds
- M is Positive
let M be Matrix of n, REAL ; ::_thesis: ( M is Negative implies - M is Positive )
A1: ( Indices M = [:(Seg n),(Seg n):] & Indices (- M) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A2: M is Negative ; ::_thesis: - M is Positive
 for i, j being Nat st [i,j] in Indices (- M) holds
(- M) * (i,j) > 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M) implies (- M) * (i,j) > 0 )
assume A3: [i,j] in Indices (- M) ; ::_thesis: (- M) * (i,j) > 0
then  M * (i,j) < 0 by A2, A1, Def2;
then  - (M * (i,j)) > 0 by XREAL_1:58;
hence  (- M) * (i,j) > 0 by A1, A3, Th2; ::_thesis: verum
end;
hence  - M is Positive by Def1; ::_thesis: verum
end;

theorem :: MATRIX10:8
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Positive holds
M1 + M2 is Positive
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Positive holds
M1 + M2 is Positive
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive & M2 is Positive implies M1 + M2 is Positive )
A1: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 + M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A3: ( M1 is Positive & M2 is Positive ) ; ::_thesis: M1 + M2 is Positive
 for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) > 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) > 0 )
assume A4: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) > 0
then  ( M1 * (i,j) > 0 & M2 * (i,j) > 0 ) by A3, A1, A2, Def1;
then  (M1 * (i,j)) + (M2 * (i,j)) > 0 ;
hence  (M1 + M2) * (i,j) > 0 by A2, A4, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 + M2 is Positive by Def1; ::_thesis: verum
end;

theorem :: MATRIX10:9
for n being Nat
for M2, M1 being Matrix of n, REAL st - M2 is_less_than M1 holds
M1 + M2 is Positive
proof
let n be Nat; ::_thesis: for M2, M1 being Matrix of n, REAL st - M2 is_less_than M1 holds
M1 + M2 is Positive
let M2, M1 be Matrix of n, REAL ; ::_thesis: ( - M2 is_less_than M1 implies M1 + M2 is Positive )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices (- M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A4: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume A5: - M2 is_less_than M1 ; ::_thesis: M1 + M2 is Positive
 for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) > 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) > 0 )
assume A6: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) > 0
then  (- M2) * (i,j) < M1 * (i,j) by A5, A3, A4, Def5;
then  - (M2 * (i,j)) < M1 * (i,j) by A2, A4, A6, Th2;
then  (M1 * (i,j)) + (M2 * (i,j)) > 0 by XREAL_1:62;
hence  (M1 + M2) * (i,j) > 0 by A1, A4, A6, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 + M2 is Positive by Def1; ::_thesis: verum
end;

theorem :: MATRIX10:10
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Nonnegative & M2 is Positive holds
M1 + M2 is Positive
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Nonnegative & M2 is Positive holds
M1 + M2 is Positive
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonnegative & M2 is Positive implies M1 + M2 is Positive )
A1: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 + M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A3: ( M1 is Nonnegative & M2 is Positive ) ; ::_thesis: M1 + M2 is Positive
 for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) > 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) > 0 )
assume A4: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) > 0
then  ( M1 * (i,j) >= 0 & M2 * (i,j) > 0 ) by A3, A1, A2, Def1, Def4;
then  (M1 * (i,j)) + (M2 * (i,j)) > 0 ;
hence  (M1 + M2) * (i,j) > 0 by A2, A4, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 + M2 is Positive by Def1; ::_thesis: verum
end;

theorem :: MATRIX10:11
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative & |:M2:| is_less_than |:M1:| holds
M1 + M2 is Positive
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative & |:M2:| is_less_than |:M1:| holds
M1 + M2 is Positive
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive & M2 is Negative & |:M2:| is_less_than |:M1:| implies M1 + M2 is Positive )
assume that
A1: M1 is Positive and
A2: M2 is Negative and
A3: |:M2:| is_less_than |:M1:| ; ::_thesis: M1 + M2 is Positive
A4: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) > 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) > 0 )
assume A7: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) > 0
then  [i,j] in Indices |:M2:| by A4, A5, Th5;
then  |:M2:| * (i,j) < |:M1:| * (i,j) by A3, Def5;
then  abs (M2 * (i,j)) < |:M1:| * (i,j) by A4, A5, A7, Def7;
then  abs (M2 * (i,j)) < abs (M1 * (i,j)) by A6, A5, A7, Def7;
then A8: (abs (M1 * (i,j))) - (abs (M2 * (i,j))) > 0 by XREAL_1:50;
 M2 * (i,j) < 0 by A2, A4, A5, A7, Def2;
then A9: - (M2 * (i,j)) = abs (M2 * (i,j)) by ABSVALUE:def_1;
 M1 * (i,j) > 0 by A1, A6, A5, A7, Def1;
then  M1 * (i,j) = abs (M1 * (i,j)) by ABSVALUE:def_1;
then  (M1 * (i,j)) + (M2 * (i,j)) > 0 by A9, A8;
hence  (M1 + M2) * (i,j) > 0 by A6, A5, A7, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 + M2 is Positive by Def1; ::_thesis: verum
end;

theorem :: MATRIX10:12
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative holds
M1 - M2 is Positive
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative holds
M1 - M2 is Positive
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive & M2 is Negative implies M1 - M2 is Positive )
assume A1: ( M1 is Positive & M2 is Negative ) ; ::_thesis: M1 - M2 is Positive
A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 - M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
A4: ( len M1 = len M2 & width M1 = width M2 ) by Lm1;
 for i, j being Nat st [i,j] in Indices (M1 - M2) holds
(M1 - M2) * (i,j) > 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M2) implies (M1 - M2) * (i,j) > 0 )
assume A5: [i,j] in Indices (M1 - M2) ; ::_thesis: (M1 - M2) * (i,j) > 0
then  ( M1 * (i,j) > 0 & M2 * (i,j) < 0 ) by A1, A2, A3, Def1, Def2;
then  (M1 * (i,j)) - (M2 * (i,j)) > 0 - 0 ;
hence  (M1 - M2) * (i,j) > 0 by A3, A4, A5, Th3; ::_thesis: verum
end;
hence  M1 - M2 is Positive by Def1; ::_thesis: verum
end;

theorem :: MATRIX10:13
for n being Nat
for M2, M1 being Matrix of n, REAL st M2 is_less_than M1 holds
M1 - M2 is Positive
proof
let n be Nat; ::_thesis: for M2, M1 being Matrix of n, REAL st M2 is_less_than M1 holds
M1 - M2 is Positive
let M2, M1 be Matrix of n, REAL ; ::_thesis: ( M2 is_less_than M1 implies M1 - M2 is Positive )
assume A1: M2 is_less_than M1 ; ::_thesis: M1 - M2 is Positive
A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: width M1 = width M2 by Lm1;
A4: Indices (M1 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: ( Indices M1 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (M1 - M2) holds
(M1 - M2) * (i,j) > 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M2) implies (M1 - M2) * (i,j) > 0 )
assume A6: [i,j] in Indices (M1 - M2) ; ::_thesis: (M1 - M2) * (i,j) > 0
then  M1 * (i,j) > M2 * (i,j) by A1, A2, A4, Def5;
then  (M1 * (i,j)) - (M2 * (i,j)) > 0 by XREAL_1:50;
hence  (M1 - M2) * (i,j) > 0 by A4, A5, A3, A6, Th3; ::_thesis: verum
end;
hence  M1 - M2 is Positive by Def1; ::_thesis: verum
end;

theorem :: MATRIX10:14
for a being Element of REAL
for n being Nat
for M being Matrix of n, REAL st a > 0 & M is Positive holds
a * M is Positive
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M being Matrix of n, REAL st a > 0 & M is Positive holds
a * M is Positive
let n be Nat; ::_thesis: for M being Matrix of n, REAL st a > 0 & M is Positive holds
a * M is Positive
let M be Matrix of n, REAL ; ::_thesis: ( a > 0 & M is Positive implies a * M is Positive )
assume that
A1: a > 0 and
A2: M is Positive ; ::_thesis: a * M is Positive
 for i, j being Nat st [i,j] in Indices (a * M) holds
(a * M) * (i,j) > 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) > 0 )
assume  [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) > 0
then A3: [i,j] in Indices M by MATRIXR1:28;
then  M * (i,j) > 0 by A2, Def1;
then  a * (M * (i,j)) > 0 by A1, XREAL_1:129;
hence  (a * M) * (i,j) > 0 by A3, Th4; ::_thesis: verum
end;
hence  a * M is Positive by Def1; ::_thesis: verum
end;

theorem :: MATRIX10:15
for a being Element of REAL
for n being Nat
for M being Matrix of n, REAL st a < 0 & M is Negative holds
a * M is Positive
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M being Matrix of n, REAL st a < 0 & M is Negative holds
a * M is Positive
let n be Nat; ::_thesis: for M being Matrix of n, REAL st a < 0 & M is Negative holds
a * M is Positive
let M be Matrix of n, REAL ; ::_thesis: ( a < 0 & M is Negative implies a * M is Positive )
assume that
A1: a < 0 and
A2: M is Negative ; ::_thesis: a * M is Positive
A3: Indices (a * M) = Indices M by MATRIXR1:28;
 for i, j being Nat st [i,j] in Indices (a * M) holds
(a * M) * (i,j) > 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) > 0 )
assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) > 0
then  M * (i,j) < 0 by A2, A3, Def2;
then  a * (M * (i,j)) > 0 by A1, XREAL_1:130;
hence  (a * M) * (i,j) > 0 by A3, A4, Th4; ::_thesis: verum
end;
hence  a * M is Positive by Def1; ::_thesis: verum
end;

theorem :: MATRIX10:16
for n being Nat
for M being Matrix of n, REAL st M is Positive holds
- M is Negative
proof
let n be Nat; ::_thesis: for M being Matrix of n, REAL st M is Positive holds
- M is Negative
let M be Matrix of n, REAL ; ::_thesis: ( M is Positive implies - M is Negative )
A1: ( Indices M = [:(Seg n),(Seg n):] & Indices (- M) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A2: M is Positive ; ::_thesis: - M is Negative
 for i, j being Nat st [i,j] in Indices (- M) holds
(- M) * (i,j) < 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M) implies (- M) * (i,j) < 0 )
assume A3: [i,j] in Indices (- M) ; ::_thesis: (- M) * (i,j) < 0
then  M * (i,j) > 0 by A2, A1, Def1;
then  (- 1) * (M * (i,j)) < 0 * (- 1) by XREAL_1:69;
then  - (M * (i,j)) < 0 ;
hence  (- M) * (i,j) < 0 by A1, A3, Th2; ::_thesis: verum
end;
hence  - M is Negative by Def2; ::_thesis: verum
end;

theorem :: MATRIX10:17
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Negative & M2 is Negative holds
M1 + M2 is Negative
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Negative & M2 is Negative holds
M1 + M2 is Negative
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Negative & M2 is Negative implies M1 + M2 is Negative )
assume that
A1: M1 is Negative and
A2: M2 is Negative ; ::_thesis: M1 + M2 is Negative
A3: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A4: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) < 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) < 0 )
assume A6: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) < 0
then  M1 * (i,j) < 0 by A1, A3, A4, Def2;
then  (M1 * (i,j)) + (M2 * (i,j)) < M2 * (i,j) by XREAL_1:30;
then  (M1 * (i,j)) + (M2 * (i,j)) < 0 by A2, A5, A4, A6, Def2;
hence  (M1 + M2) * (i,j) < 0 by A3, A4, A6, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 + M2 is Negative by Def2; ::_thesis: verum
end;

theorem :: MATRIX10:18
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_than - M2 holds
M1 + M2 is Negative
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than - M2 holds
M1 + M2 is Negative
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than - M2 implies M1 + M2 is Negative )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume A4: M1 is_less_than - M2 ; ::_thesis: M1 + M2 is Negative
 for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) < 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) < 0 )
assume A5: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) < 0
then  M1 * (i,j) < (- M2) * (i,j) by A4, A1, A3, Def5;
then  M1 * (i,j) < - (M2 * (i,j)) by A2, A3, A5, Th2;
then  (M1 * (i,j)) + (M2 * (i,j)) < 0 by XREAL_1:61;
hence  (M1 + M2) * (i,j) < 0 by A1, A3, A5, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 + M2 is Negative by Def2; ::_thesis: verum
end;

theorem :: MATRIX10:19
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative & |:M1:| is_less_than |:M2:| holds
M1 + M2 is Negative
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative & |:M1:| is_less_than |:M2:| holds
M1 + M2 is Negative
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive & M2 is Negative & |:M1:| is_less_than |:M2:| implies M1 + M2 is Negative )
assume that
A1: M1 is Positive and
A2: M2 is Negative and
A3: |:M1:| is_less_than |:M2:| ; ::_thesis: M1 + M2 is Negative
A4: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) < 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) < 0 )
assume A7: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) < 0
then  [i,j] in Indices |:M1:| by A4, A5, Th5;
then  |:M1:| * (i,j) < |:M2:| * (i,j) by A3, Def5;
then  abs (M1 * (i,j)) < |:M2:| * (i,j) by A4, A5, A7, Def7;
then  abs (M1 * (i,j)) < abs (M2 * (i,j)) by A6, A5, A7, Def7;
then A8: (abs (M1 * (i,j))) - (abs (M2 * (i,j))) < (abs (M2 * (i,j))) - (abs (M2 * (i,j))) by XREAL_1:9;
 M2 * (i,j) < 0 by A2, A6, A5, A7, Def2;
then A9: - (M2 * (i,j)) = abs (M2 * (i,j)) by ABSVALUE:def_1;
 M1 * (i,j) > 0 by A1, A4, A5, A7, Def1;
then  abs (M1 * (i,j)) = M1 * (i,j) by ABSVALUE:def_1;
then  (M1 * (i,j)) + (M2 * (i,j)) = (abs (M1 * (i,j))) - (abs (M2 * (i,j))) by A9;
hence  (M1 + M2) * (i,j) < 0 by A4, A5, A7, A8, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 + M2 is Negative by Def2; ::_thesis: verum
end;

theorem :: MATRIX10:20
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 holds
M1 - M2 is Negative
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 holds
M1 - M2 is Negative
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 implies M1 - M2 is Negative )
assume A1: M1 is_less_than M2 ; ::_thesis: M1 - M2 is Negative
A2: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 - M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
A3: ( len M1 = len M2 & width M1 = width M2 ) by Lm1;
 for i, j being Nat st [i,j] in Indices (M1 - M2) holds
(M1 - M2) * (i,j) < 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M2) implies (M1 - M2) * (i,j) < 0 )
assume A4: [i,j] in Indices (M1 - M2) ; ::_thesis: (M1 - M2) * (i,j) < 0
then  M1 * (i,j) < M2 * (i,j) by A1, A2, Def5;
then  (M1 * (i,j)) - (M2 * (i,j)) < 0 by XREAL_1:49;
hence  (M1 - M2) * (i,j) < 0 by A2, A3, A4, Th3; ::_thesis: verum
end;
hence  M1 - M2 is Negative by Def2; ::_thesis: verum
end;

theorem :: MATRIX10:21
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative holds
M2 - M1 is Negative
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative holds
M2 - M1 is Negative
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive & M2 is Negative implies M2 - M1 is Negative )
assume A1: ( M1 is Positive & M2 is Negative ) ; ::_thesis: M2 - M1 is Negative
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: ( Indices M2 = [:(Seg n),(Seg n):] & Indices (M2 - M1) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
A4: ( len M1 = len M2 & width M1 = width M2 ) by Lm1;
 for i, j being Nat st [i,j] in Indices (M2 - M1) holds
(M2 - M1) * (i,j) < 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M2 - M1) implies (M2 - M1) * (i,j) < 0 )
assume A5: [i,j] in Indices (M2 - M1) ; ::_thesis: (M2 - M1) * (i,j) < 0
then  ( M1 * (i,j) > 0 & M2 * (i,j) < 0 ) by A1, A2, A3, Def1, Def2;
then  (M2 * (i,j)) - (M1 * (i,j)) < 0 ;
hence  (M2 - M1) * (i,j) < 0 by A3, A4, A5, Th3; ::_thesis: verum
end;
hence  M2 - M1 is Negative by Def2; ::_thesis: verum
end;

theorem :: MATRIX10:22
for a being Element of REAL
for n being Nat
for M being Matrix of n, REAL st a < 0 & M is Positive holds
a * M is Negative
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M being Matrix of n, REAL st a < 0 & M is Positive holds
a * M is Negative
let n be Nat; ::_thesis: for M being Matrix of n, REAL st a < 0 & M is Positive holds
a * M is Negative
let M be Matrix of n, REAL ; ::_thesis: ( a < 0 & M is Positive implies a * M is Negative )
assume that
A1: a < 0 and
A2: M is Positive ; ::_thesis: a * M is Negative
A3: Indices (a * M) = Indices M by MATRIXR1:28;
 for i, j being Nat st [i,j] in Indices (a * M) holds
(a * M) * (i,j) < 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) < 0 )
assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) < 0
then  M * (i,j) > 0 by A2, A3, Def1;
then  a * (M * (i,j)) < 0 by A1, XREAL_1:132;
hence  (a * M) * (i,j) < 0 by A3, A4, Th4; ::_thesis: verum
end;
hence  a * M is Negative by Def2; ::_thesis: verum
end;

theorem :: MATRIX10:23
for a being Element of REAL
for n being Nat
for M being Matrix of n, REAL st a > 0 & M is Negative holds
a * M is Negative
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M being Matrix of n, REAL st a > 0 & M is Negative holds
a * M is Negative
let n be Nat; ::_thesis: for M being Matrix of n, REAL st a > 0 & M is Negative holds
a * M is Negative
let M be Matrix of n, REAL ; ::_thesis: ( a > 0 & M is Negative implies a * M is Negative )
assume that
A1: a > 0 and
A2: M is Negative ; ::_thesis: a * M is Negative
A3: Indices (a * M) = Indices M by MATRIXR1:28;
 for i, j being Nat st [i,j] in Indices (a * M) holds
(a * M) * (i,j) < 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) < 0 )
assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) < 0
then  M * (i,j) < 0 by A2, A3, Def2;
then  a * (M * (i,j)) < 0 by A1, XREAL_1:132;
hence  (a * M) * (i,j) < 0 by A3, A4, Th4; ::_thesis: verum
end;
hence  a * M is Negative by Def2; ::_thesis: verum
end;

theorem :: MATRIX10:24
for n being Nat
for M being Matrix of n, REAL st M is Nonnegative holds
- M is Nonpositive
proof
let n be Nat; ::_thesis: for M being Matrix of n, REAL st M is Nonnegative holds
- M is Nonpositive
let M be Matrix of n, REAL ; ::_thesis: ( M is Nonnegative implies - M is Nonpositive )
A1: ( Indices M = [:(Seg n),(Seg n):] & Indices (- M) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A2: M is Nonnegative ; ::_thesis: - M is Nonpositive
 for i, j being Nat st [i,j] in Indices (- M) holds
(- M) * (i,j) <= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M) implies (- M) * (i,j) <= 0 )
assume A3: [i,j] in Indices (- M) ; ::_thesis: (- M) * (i,j) <= 0
then  M * (i,j) >= 0 by A2, A1, Def4;
then  - (M * (i,j)) <= 0 ;
hence  (- M) * (i,j) <= 0 by A1, A3, Th2; ::_thesis: verum
end;
hence  - M is Nonpositive by Def3; ::_thesis: verum
end;

theorem :: MATRIX10:25
for n being Nat
for M being Matrix of n, REAL st M is Negative holds
M is Nonpositive
proof
let n be Nat; ::_thesis: for M being Matrix of n, REAL st M is Negative holds
M is Nonpositive
let M be Matrix of n, REAL ; ::_thesis: ( M is Negative implies M is Nonpositive )
assume  M is Negative ; ::_thesis: M is Nonpositive
then  for i, j being Nat st [i,j] in Indices M holds
M * (i,j) <= 0 by Def2;
hence  M is Nonpositive by Def3; ::_thesis: verum
end;

theorem :: MATRIX10:26
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Nonpositive & M2 is Nonpositive holds
M1 + M2 is Nonpositive
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Nonpositive & M2 is Nonpositive holds
M1 + M2 is Nonpositive
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonpositive & M2 is Nonpositive implies M1 + M2 is Nonpositive )
assume that
A1: M1 is Nonpositive and
A2: M2 is Nonpositive ; ::_thesis: M1 + M2 is Nonpositive
A3: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A4: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) <= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) <= 0 )
assume A6: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) <= 0
then  M1 * (i,j) <= 0 by A1, A3, A4, Def3;
then A7: (M1 * (i,j)) + (M2 * (i,j)) <= M2 * (i,j) by XREAL_1:32;
 M2 * (i,j) <= 0 by A2, A5, A4, A6, Def3;
hence  (M1 + M2) * (i,j) <= 0 by A3, A4, A6, A7, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 + M2 is Nonpositive by Def3; ::_thesis: verum
end;

theorem :: MATRIX10:27
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with - M2 holds
M1 + M2 is Nonpositive
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with - M2 holds
M1 + M2 is Nonpositive
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with - M2 implies M1 + M2 is Nonpositive )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume A4: M1 is_less_or_equal_with - M2 ; ::_thesis: M1 + M2 is Nonpositive
 for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) <= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) <= 0 )
assume A5: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) <= 0
then  M1 * (i,j) <= (- M2) * (i,j) by A4, A1, A3, Def6;
then  M1 * (i,j) <= - (M2 * (i,j)) by A2, A3, A5, Th2;
then  (M1 * (i,j)) + (M2 * (i,j)) <= 0 by XREAL_1:59;
hence  (M1 + M2) * (i,j) <= 0 by A1, A3, A5, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 + M2 is Nonpositive by Def3; ::_thesis: verum
end;

theorem :: MATRIX10:28
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds
M1 - M2 is Nonpositive
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds
M1 - M2 is Nonpositive
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 implies M1 - M2 is Nonpositive )
assume A1: M1 is_less_or_equal_with M2 ; ::_thesis: M1 - M2 is Nonpositive
A2: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 - M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
A3: ( len M1 = len M2 & width M1 = width M2 ) by Lm1;
 for i, j being Nat st [i,j] in Indices (M1 - M2) holds
(M1 - M2) * (i,j) <= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M2) implies (M1 - M2) * (i,j) <= 0 )
assume A4: [i,j] in Indices (M1 - M2) ; ::_thesis: (M1 - M2) * (i,j) <= 0
then  M1 * (i,j) <= M2 * (i,j) by A1, A2, Def6;
then  (M1 * (i,j)) - (M2 * (i,j)) <= 0 by XREAL_1:47;
hence  (M1 - M2) * (i,j) <= 0 by A2, A3, A4, Th3; ::_thesis: verum
end;
hence  M1 - M2 is Nonpositive by Def3; ::_thesis: verum
end;

theorem :: MATRIX10:29
for a being Element of REAL
for n being Nat
for M being Matrix of n, REAL st a <= 0 & M is Positive holds
a * M is Nonpositive
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M being Matrix of n, REAL st a <= 0 & M is Positive holds
a * M is Nonpositive
let n be Nat; ::_thesis: for M being Matrix of n, REAL st a <= 0 & M is Positive holds
a * M is Nonpositive
let M be Matrix of n, REAL ; ::_thesis: ( a <= 0 & M is Positive implies a * M is Nonpositive )
assume that
A1: a <= 0 and
A2: M is Positive ; ::_thesis: a * M is Nonpositive
A3: Indices (a * M) = Indices M by MATRIXR1:28;
 for i, j being Nat st [i,j] in Indices (a * M) holds
(a * M) * (i,j) <= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) <= 0 )
assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) <= 0
then  M * (i,j) > 0 by A2, A3, Def1;
then  a * (M * (i,j)) <= 0 by A1;
hence  (a * M) * (i,j) <= 0 by A3, A4, Th4; ::_thesis: verum
end;
hence  a * M is Nonpositive by Def3; ::_thesis: verum
end;

theorem :: MATRIX10:30
for a being Element of REAL
for n being Nat
for M being Matrix of n, REAL st a >= 0 & M is Negative holds
a * M is Nonpositive
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M being Matrix of n, REAL st a >= 0 & M is Negative holds
a * M is Nonpositive
let n be Nat; ::_thesis: for M being Matrix of n, REAL st a >= 0 & M is Negative holds
a * M is Nonpositive
let M be Matrix of n, REAL ; ::_thesis: ( a >= 0 & M is Negative implies a * M is Nonpositive )
assume that
A1: a >= 0 and
A2: M is Negative ; ::_thesis: a * M is Nonpositive
A3: Indices (a * M) = Indices M by MATRIXR1:28;
 for i, j being Nat st [i,j] in Indices (a * M) holds
(a * M) * (i,j) <= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) <= 0 )
assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) <= 0
then  M * (i,j) < 0 by A2, A3, Def2;
then  a * (M * (i,j)) <= 0 by A1;
hence  (a * M) * (i,j) <= 0 by A3, A4, Th4; ::_thesis: verum
end;
hence  a * M is Nonpositive by Def3; ::_thesis: verum
end;

theorem :: MATRIX10:31
for a being Element of REAL
for n being Nat
for M being Matrix of n, REAL st a >= 0 & M is Nonpositive holds
a * M is Nonpositive
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M being Matrix of n, REAL st a >= 0 & M is Nonpositive holds
a * M is Nonpositive
let n be Nat; ::_thesis: for M being Matrix of n, REAL st a >= 0 & M is Nonpositive holds
a * M is Nonpositive
let M be Matrix of n, REAL ; ::_thesis: ( a >= 0 & M is Nonpositive implies a * M is Nonpositive )
assume that
A1: a >= 0 and
A2: M is Nonpositive ; ::_thesis: a * M is Nonpositive
A3: Indices (a * M) = Indices M by MATRIXR1:28;
 for i, j being Nat st [i,j] in Indices (a * M) holds
(a * M) * (i,j) <= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) <= 0 )
assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) <= 0
then  M * (i,j) <= 0 by A2, A3, Def3;
then  a * (M * (i,j)) <= 0 by A1;
hence  (a * M) * (i,j) <= 0 by A3, A4, Th4; ::_thesis: verum
end;
hence  a * M is Nonpositive by Def3; ::_thesis: verum
end;

theorem :: MATRIX10:32
for a being Element of REAL
for n being Nat
for M being Matrix of n, REAL st a <= 0 & M is Nonnegative holds
a * M is Nonpositive
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M being Matrix of n, REAL st a <= 0 & M is Nonnegative holds
a * M is Nonpositive
let n be Nat; ::_thesis: for M being Matrix of n, REAL st a <= 0 & M is Nonnegative holds
a * M is Nonpositive
let M be Matrix of n, REAL ; ::_thesis: ( a <= 0 & M is Nonnegative implies a * M is Nonpositive )
assume that
A1: a <= 0 and
A2: M is Nonnegative ; ::_thesis: a * M is Nonpositive
A3: Indices (a * M) = Indices M by MATRIXR1:28;
 for i, j being Nat st [i,j] in Indices (a * M) holds
(a * M) * (i,j) <= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) <= 0 )
assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) <= 0
then  M * (i,j) >= 0 by A2, A3, Def4;
then  a * (M * (i,j)) <= 0 by A1;
hence  (a * M) * (i,j) <= 0 by A3, A4, Th4; ::_thesis: verum
end;
hence  a * M is Nonpositive by Def3; ::_thesis: verum
end;

theorem :: MATRIX10:33
for n being Nat
for M being Matrix of n, REAL holds |:M:| is Nonnegative
proof
let n be Nat; ::_thesis: for M being Matrix of n, REAL holds |:M:| is Nonnegative
let M be Matrix of n, REAL ; ::_thesis: |:M:| is Nonnegative
 for i, j being Nat st [i,j] in Indices |:M:| holds
|:M:| * (i,j) >= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices |:M:| implies |:M:| * (i,j) >= 0 )
assume A1: [i,j] in Indices |:M:| ; ::_thesis: |:M:| * (i,j) >= 0
 Indices |:M:| = Indices M by Th5;
then  |:M:| * (i,j) = abs (M * (i,j)) by A1, Def7;
hence  |:M:| * (i,j) >= 0 by COMPLEX1:46; ::_thesis: verum
end;
hence  |:M:| is Nonnegative by Def4; ::_thesis: verum
end;

theorem :: MATRIX10:34
for n being Nat
for M1 being Matrix of n, REAL st M1 is Positive holds
M1 is Nonnegative
proof
let n be Nat; ::_thesis: for M1 being Matrix of n, REAL st M1 is Positive holds
M1 is Nonnegative
let M1 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive implies M1 is Nonnegative )
assume  M1 is Positive ; ::_thesis: M1 is Nonnegative
then  for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) >= 0 by Def1;
hence  M1 is Nonnegative by Def4; ::_thesis: verum
end;

theorem :: MATRIX10:35
for n being Nat
for M being Matrix of n, REAL st M is Nonpositive holds
- M is Nonnegative
proof
let n be Nat; ::_thesis: for M being Matrix of n, REAL st M is Nonpositive holds
- M is Nonnegative
let M be Matrix of n, REAL ; ::_thesis: ( M is Nonpositive implies - M is Nonnegative )
A1: ( Indices M = [:(Seg n),(Seg n):] & Indices (- M) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A2: M is Nonpositive ; ::_thesis: - M is Nonnegative
 for i, j being Nat st [i,j] in Indices (- M) holds
(- M) * (i,j) >= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M) implies (- M) * (i,j) >= 0 )
assume A3: [i,j] in Indices (- M) ; ::_thesis: (- M) * (i,j) >= 0
then  M * (i,j) <= 0 by A2, A1, Def3;
then  - (M * (i,j)) >= 0 ;
hence  (- M) * (i,j) >= 0 by A1, A3, Th2; ::_thesis: verum
end;
hence  - M is Nonnegative by Def4; ::_thesis: verum
end;

theorem Th36: :: MATRIX10:36
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Nonnegative & M2 is Nonnegative holds
M1 + M2 is Nonnegative
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Nonnegative & M2 is Nonnegative holds
M1 + M2 is Nonnegative
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonnegative & M2 is Nonnegative implies M1 + M2 is Nonnegative )
A1: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 + M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A3: ( M1 is Nonnegative & M2 is Nonnegative ) ; ::_thesis: M1 + M2 is Nonnegative
 for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) >= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) >= 0 )
assume A4: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) >= 0
then  ( M1 * (i,j) >= 0 & M2 * (i,j) >= 0 ) by A3, A1, A2, Def4;
then  (M1 * (i,j)) + (M2 * (i,j)) >= 0 ;
hence  (M1 + M2) * (i,j) >= 0 by A2, A4, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 + M2 is Nonnegative by Def4; ::_thesis: verum
end;

theorem :: MATRIX10:37
for n being Nat
for M1, M2 being Matrix of n, REAL st - M1 is_less_or_equal_with M2 holds
M1 + M2 is Nonnegative
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st - M1 is_less_or_equal_with M2 holds
M1 + M2 is Nonnegative
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( - M1 is_less_or_equal_with M2 implies M1 + M2 is Nonnegative )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: Indices (- M1) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume A4: - M1 is_less_or_equal_with M2 ; ::_thesis: M1 + M2 is Nonnegative
 for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) >= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) >= 0 )
assume A5: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) >= 0
then  (- M1) * (i,j) <= M2 * (i,j) by A4, A2, A3, Def6;
then  - (M1 * (i,j)) <= M2 * (i,j) by A1, A3, A5, Th2;
then  (M1 * (i,j)) + (M2 * (i,j)) >= 0 by XREAL_1:60;
hence  (M1 + M2) * (i,j) >= 0 by A1, A3, A5, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 + M2 is Nonnegative by Def4; ::_thesis: verum
end;

theorem :: MATRIX10:38
for n being Nat
for M2, M1 being Matrix of n, REAL st M2 is_less_or_equal_with M1 holds
M1 - M2 is Nonnegative
proof
let n be Nat; ::_thesis: for M2, M1 being Matrix of n, REAL st M2 is_less_or_equal_with M1 holds
M1 - M2 is Nonnegative
let M2, M1 be Matrix of n, REAL ; ::_thesis: ( M2 is_less_or_equal_with M1 implies M1 - M2 is Nonnegative )
assume A1: M2 is_less_or_equal_with M1 ; ::_thesis: M1 - M2 is Nonnegative
A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: width M1 = width M2 by Lm1;
A4: Indices (M1 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: ( Indices M1 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (M1 - M2) holds
(M1 - M2) * (i,j) >= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M2) implies (M1 - M2) * (i,j) >= 0 )
assume A6: [i,j] in Indices (M1 - M2) ; ::_thesis: (M1 - M2) * (i,j) >= 0
then  M1 * (i,j) >= M2 * (i,j) by A1, A2, A4, Def6;
then  (M1 * (i,j)) - (M2 * (i,j)) >= 0 by XREAL_1:48;
hence  (M1 - M2) * (i,j) >= 0 by A4, A5, A3, A6, Th3; ::_thesis: verum
end;
hence  M1 - M2 is Nonnegative by Def4; ::_thesis: verum
end;

theorem :: MATRIX10:39
for a being Element of REAL
for n being Nat
for M being Matrix of n, REAL st a >= 0 & M is Positive holds
a * M is Nonnegative
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M being Matrix of n, REAL st a >= 0 & M is Positive holds
a * M is Nonnegative
let n be Nat; ::_thesis: for M being Matrix of n, REAL st a >= 0 & M is Positive holds
a * M is Nonnegative
let M be Matrix of n, REAL ; ::_thesis: ( a >= 0 & M is Positive implies a * M is Nonnegative )
assume that
A1: a >= 0 and
A2: M is Positive ; ::_thesis: a * M is Nonnegative
 for i, j being Nat st [i,j] in Indices (a * M) holds
(a * M) * (i,j) >= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) >= 0 )
assume  [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) >= 0
then A3: [i,j] in Indices M by MATRIXR1:28;
then  M * (i,j) > 0 by A2, Def1;
then  a * (M * (i,j)) >= 0 by A1;
hence  (a * M) * (i,j) >= 0 by A3, Th4; ::_thesis: verum
end;
hence  a * M is Nonnegative by Def4; ::_thesis: verum
end;

theorem :: MATRIX10:40
for a being Element of REAL
for n being Nat
for M being Matrix of n, REAL st a <= 0 & M is Negative holds
a * M is Nonnegative
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M being Matrix of n, REAL st a <= 0 & M is Negative holds
a * M is Nonnegative
let n be Nat; ::_thesis: for M being Matrix of n, REAL st a <= 0 & M is Negative holds
a * M is Nonnegative
let M be Matrix of n, REAL ; ::_thesis: ( a <= 0 & M is Negative implies a * M is Nonnegative )
assume that
A1: a <= 0 and
A2: M is Negative ; ::_thesis: a * M is Nonnegative
A3: Indices (a * M) = Indices M by MATRIXR1:28;
 for i, j being Nat st [i,j] in Indices (a * M) holds
(a * M) * (i,j) >= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) >= 0 )
assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) >= 0
then  M * (i,j) < 0 by A2, A3, Def2;
then  a * (M * (i,j)) >= 0 by A1;
hence  (a * M) * (i,j) >= 0 by A3, A4, Th4; ::_thesis: verum
end;
hence  a * M is Nonnegative by Def4; ::_thesis: verum
end;

theorem :: MATRIX10:41
for a being Element of REAL
for n being Nat
for M being Matrix of n, REAL st a <= 0 & M is Nonpositive holds
a * M is Nonnegative
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M being Matrix of n, REAL st a <= 0 & M is Nonpositive holds
a * M is Nonnegative
let n be Nat; ::_thesis: for M being Matrix of n, REAL st a <= 0 & M is Nonpositive holds
a * M is Nonnegative
let M be Matrix of n, REAL ; ::_thesis: ( a <= 0 & M is Nonpositive implies a * M is Nonnegative )
assume that
A1: a <= 0 and
A2: M is Nonpositive ; ::_thesis: a * M is Nonnegative
A3: Indices (a * M) = Indices M by MATRIXR1:28;
 for i, j being Nat st [i,j] in Indices (a * M) holds
(a * M) * (i,j) >= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) >= 0 )
assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) >= 0
then  M * (i,j) <= 0 by A2, A3, Def3;
then  a * (M * (i,j)) >= 0 by A1;
hence  (a * M) * (i,j) >= 0 by A3, A4, Th4; ::_thesis: verum
end;
hence  a * M is Nonnegative by Def4; ::_thesis: verum
end;

theorem Th42: :: MATRIX10:42
for a being Element of REAL
for n being Nat
for M being Matrix of n, REAL st a >= 0 & M is Nonnegative holds
a * M is Nonnegative
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M being Matrix of n, REAL st a >= 0 & M is Nonnegative holds
a * M is Nonnegative
let n be Nat; ::_thesis: for M being Matrix of n, REAL st a >= 0 & M is Nonnegative holds
a * M is Nonnegative
let M be Matrix of n, REAL ; ::_thesis: ( a >= 0 & M is Nonnegative implies a * M is Nonnegative )
assume that
A1: a >= 0 and
A2: M is Nonnegative ; ::_thesis: a * M is Nonnegative
A3: Indices (a * M) = Indices M by MATRIXR1:28;
 for i, j being Nat st [i,j] in Indices (a * M) holds
(a * M) * (i,j) >= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) >= 0 )
assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) >= 0
then  M * (i,j) >= 0 by A2, A3, Def4;
then  a * (M * (i,j)) >= 0 by A1;
hence  (a * M) * (i,j) >= 0 by A3, A4, Th4; ::_thesis: verum
end;
hence  a * M is Nonnegative by Def4; ::_thesis: verum
end;

theorem :: MATRIX10:43
for a, b being Element of REAL
for n being Nat
for M1, M2 being Matrix of n, REAL st a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative holds
(a * M1) + (b * M2) is Nonnegative
proof
let a, b be Element of REAL ; ::_thesis: for n being Nat
for M1, M2 being Matrix of n, REAL st a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative holds
(a * M1) + (b * M2) is Nonnegative
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative holds
(a * M1) + (b * M2) is Nonnegative
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative implies (a * M1) + (b * M2) is Nonnegative )
assume  ( a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative ) ; ::_thesis: (a * M1) + (b * M2) is Nonnegative
then  ( a * M1 is Nonnegative & b * M2 is Nonnegative ) by Th42;
hence  (a * M1) + (b * M2) is Nonnegative by Th36; ::_thesis: verum
end;

begin

theorem :: MATRIX10:44
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 holds
M1 is_less_or_equal_with M2
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 holds
M1 is_less_or_equal_with M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 implies M1 is_less_or_equal_with M2 )
assume  M1 is_less_than M2 ; ::_thesis: M1 is_less_or_equal_with M2
then  for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) <= M2 * (i,j) by Def5;
hence  M1 is_less_or_equal_with M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:45
for n being Nat
for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 & M2 is_less_than M3 holds
M1 is_less_than M3
proof
let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 & M2 is_less_than M3 holds
M1 is_less_than M3
let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 & M2 is_less_than M3 implies M1 is_less_than M3 )
A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A2: ( M1 is_less_than M2 & M2 is_less_than M3 ) ; ::_thesis: M1 is_less_than M3
 for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) < M3 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) < M3 * (i,j) )
assume  [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) < M3 * (i,j)
then  ( M1 * (i,j) < M2 * (i,j) & M2 * (i,j) < M3 * (i,j) ) by A2, A1, Def5;
hence  M1 * (i,j) < M3 * (i,j) by XXREAL_0:2; ::_thesis: verum
end;
hence  M1 is_less_than M3 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:46
for n being Nat
for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_than M2 & M3 is_less_than M4 holds
M1 + M3 is_less_than M2 + M4
proof
let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_than M2 & M3 is_less_than M4 holds
M1 + M3 is_less_than M2 + M4
let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 & M3 is_less_than M4 implies M1 + M3 is_less_than M2 + M4 )
A1: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 + M3) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A4: ( M1 is_less_than M2 & M3 is_less_than M4 ) ; ::_thesis: M1 + M3 is_less_than M2 + M4
 for i, j being Nat st [i,j] in Indices (M1 + M3) holds
(M1 + M3) * (i,j) < (M2 + M4) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M3) implies (M1 + M3) * (i,j) < (M2 + M4) * (i,j) )
assume A5: [i,j] in Indices (M1 + M3) ; ::_thesis: (M1 + M3) * (i,j) < (M2 + M4) * (i,j)
then A6: ( (M1 + M3) * (i,j) = (M1 * (i,j)) + (M3 * (i,j)) & (M2 * (i,j)) + (M4 * (i,j)) = (M2 + M4) * (i,j) ) by A1, A3, MATRIXR1:25;
 ( M1 * (i,j) < M2 * (i,j) & M3 * (i,j) < M4 * (i,j) ) by A4, A2, A3, A5, Def5;
hence  (M1 + M3) * (i,j) < (M2 + M4) * (i,j) by A6, XREAL_1:8; ::_thesis: verum
end;
hence  M1 + M3 is_less_than M2 + M4 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:47
for n being Nat
for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 holds
M1 + M3 is_less_than M2 + M3
proof
let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 holds
M1 + M3 is_less_than M2 + M3
let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 implies M1 + M3 is_less_than M2 + M3 )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices (M1 + M3) = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume A4: M1 is_less_than M2 ; ::_thesis: M1 + M3 is_less_than M2 + M3
 for i, j being Nat st [i,j] in Indices (M1 + M3) holds
(M1 + M3) * (i,j) < (M2 + M3) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M3) implies (M1 + M3) * (i,j) < (M2 + M3) * (i,j) )
assume A5: [i,j] in Indices (M1 + M3) ; ::_thesis: (M1 + M3) * (i,j) < (M2 + M3) * (i,j)
then  M1 * (i,j) < M2 * (i,j) by A4, A1, A3, Def5;
then  (M1 * (i,j)) + (M3 * (i,j)) < (M2 * (i,j)) + (M3 * (i,j)) by XREAL_1:8;
then  (M1 + M3) * (i,j) < (M2 * (i,j)) + (M3 * (i,j)) by A1, A3, A5, MATRIXR1:25;
hence  (M1 + M3) * (i,j) < (M2 + M3) * (i,j) by A2, A3, A5, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 + M3 is_less_than M2 + M3 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:48
for n being Nat
for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 holds
M3 - M2 is_less_than M3 - M1
proof
let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 holds
M3 - M2 is_less_than M3 - M1
let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 implies M3 - M2 is_less_than M3 - M1 )
assume A1: M1 is_less_than M2 ; ::_thesis: M3 - M2 is_less_than M3 - M1
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices (M3 - M1) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A4: width M2 = width M3 by Lm1;
A5: ( Indices M3 = [:(Seg n),(Seg n):] & len M2 = len M3 ) by Lm1, MATRIX_1:24;
A6: ( len M1 = len M2 & width M1 = width M2 ) by Lm1;
A7: for i, j being Nat st [i,j] in Indices (M3 - M1) holds
(M3 - M2) * (i,j) < (M3 - M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M3 - M1) implies (M3 - M2) * (i,j) < (M3 - M1) * (i,j) )
assume A8: [i,j] in Indices (M3 - M1) ; ::_thesis: (M3 - M2) * (i,j) < (M3 - M1) * (i,j)
then  M1 * (i,j) < M2 * (i,j) by A1, A2, A3, Def5;
then  (M3 * (i,j)) - (M2 * (i,j)) < (M3 * (i,j)) - (M1 * (i,j)) by XREAL_1:15;
then  (M3 - M2) * (i,j) < (M3 * (i,j)) - (M1 * (i,j)) by A3, A5, A4, A8, Th3;
hence  (M3 - M2) * (i,j) < (M3 - M1) * (i,j) by A3, A6, A5, A4, A8, Th3; ::_thesis: verum
end;
 Indices (M3 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
hence  M3 - M2 is_less_than M3 - M1 by A3, A7, Def5; ::_thesis: verum
end;

theorem :: MATRIX10:49
for n being Nat
for M1, M2 being Matrix of n, REAL holds |:(M1 + M2):| is_less_or_equal_with |:M1:| + |:M2:|
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL holds |:(M1 + M2):| is_less_or_equal_with |:M1:| + |:M2:|
let M1, M2 be Matrix of n, REAL ; ::_thesis: |:(M1 + M2):| is_less_or_equal_with |:M1:| + |:M2:|
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices |:(M1 + M2):| holds
|:(M1 + M2):| * (i,j) <= (|:M1:| + |:M2:|) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices |:(M1 + M2):| implies |:(M1 + M2):| * (i,j) <= (|:M1:| + |:M2:|) * (i,j) )
assume  [i,j] in Indices |:(M1 + M2):| ; ::_thesis: |:(M1 + M2):| * (i,j) <= (|:M1:| + |:M2:|) * (i,j)
then A4: [i,j] in Indices (M1 + M2) by Th5;
then  [i,j] in Indices |:M1:| by A1, A2, Th5;
then A5: (|:M1:| + |:M2:|) * (i,j) = (|:M1:| * (i,j)) + (|:M2:| * (i,j)) by MATRIXR1:25
.= (abs (M1 * (i,j))) + (|:M2:| * (i,j)) by A1, A2, A4, Def7
.= (abs (M1 * (i,j))) + (abs (M2 * (i,j))) by A3, A2, A4, Def7 ;
|:(M1 + M2):| * (i,j) = abs ((M1 + M2) * (i,j)) by A4, Def7
.= abs ((M1 * (i,j)) + (M2 * (i,j))) by A1, A2, A4, MATRIXR1:25 ;
hence  |:(M1 + M2):| * (i,j) <= (|:M1:| + |:M2:|) * (i,j) by A5, COMPLEX1:56; ::_thesis: verum
end;
hence  |:(M1 + M2):| is_less_or_equal_with |:M1:| + |:M2:| by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:50
for n being Nat
for M1, M2, M3 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds
M1 - M3 is_less_or_equal_with M2 - M3
proof
let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds
M1 - M3 is_less_or_equal_with M2 - M3
let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 implies M1 - M3 is_less_or_equal_with M2 - M3 )
assume A1: M1 is_less_or_equal_with M2 ; ::_thesis: M1 - M3 is_less_or_equal_with M2 - M3
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: width M2 = width M3 by Lm1;
A4: ( Indices M2 = [:(Seg n),(Seg n):] & len M2 = len M3 ) by Lm1, MATRIX_1:24;
A5: Indices (M1 - M3) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: ( len M1 = len M3 & width M1 = width M3 ) by Lm1;
 for i, j being Nat st [i,j] in Indices (M1 - M3) holds
(M1 - M3) * (i,j) <= (M2 - M3) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M3) implies (M1 - M3) * (i,j) <= (M2 - M3) * (i,j) )
assume A7: [i,j] in Indices (M1 - M3) ; ::_thesis: (M1 - M3) * (i,j) <= (M2 - M3) * (i,j)
then  M1 * (i,j) <= M2 * (i,j) by A1, A2, A5, Def6;
then  (M1 * (i,j)) - (M3 * (i,j)) <= (M2 * (i,j)) - (M3 * (i,j)) by XREAL_1:9;
then  (M1 - M3) * (i,j) <= (M2 * (i,j)) - (M3 * (i,j)) by A2, A5, A6, A7, Th3;
hence  (M1 - M3) * (i,j) <= (M2 - M3) * (i,j) by A5, A4, A3, A7, Th3; ::_thesis: verum
end;
hence  M1 - M3 is_less_or_equal_with M2 - M3 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:51
for n being Nat
for M1, M3, M2 being Matrix of n, REAL st M1 - M3 is_less_or_equal_with M2 - M3 holds
M1 is_less_or_equal_with M2
proof
let n be Nat; ::_thesis: for M1, M3, M2 being Matrix of n, REAL st M1 - M3 is_less_or_equal_with M2 - M3 holds
M1 is_less_or_equal_with M2
let M1, M3, M2 be Matrix of n, REAL ; ::_thesis: ( M1 - M3 is_less_or_equal_with M2 - M3 implies M1 is_less_or_equal_with M2 )
assume A1: M1 - M3 is_less_or_equal_with M2 - M3 ; ::_thesis: M1 is_less_or_equal_with M2
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: width M2 = width M3 by Lm1;
A4: ( Indices M2 = [:(Seg n),(Seg n):] & len M2 = len M3 ) by Lm1, MATRIX_1:24;
A5: Indices (M1 - M3) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: ( len M1 = len M3 & width M1 = width M3 ) by Lm1;
 for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) <= M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) <= M2 * (i,j) )
assume A7: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) <= M2 * (i,j)
then  (M1 - M3) * (i,j) <= (M2 - M3) * (i,j) by A1, A2, A5, Def6;
then  (M1 * (i,j)) - (M3 * (i,j)) <= (M2 - M3) * (i,j) by A6, A7, Th3;
then  (M1 * (i,j)) - (M3 * (i,j)) <= (M2 * (i,j)) - (M3 * (i,j)) by A2, A4, A3, A7, Th3;
then  ((M1 * (i,j)) - (M3 * (i,j))) + (M3 * (i,j)) <= ((M2 * (i,j)) - (M3 * (i,j))) + (M3 * (i,j)) by XREAL_1:6;
hence  M1 * (i,j) <= M2 * (i,j) ; ::_thesis: verum
end;
hence  M1 is_less_or_equal_with M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:52
for n being Nat
for M1, M2, M3 being Matrix of n, REAL st M1 is_less_or_equal_with M2 - M3 holds
M3 is_less_or_equal_with M2 - M1
proof
let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is_less_or_equal_with M2 - M3 holds
M3 is_less_or_equal_with M2 - M1
let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 - M3 implies M3 is_less_or_equal_with M2 - M1 )
assume A1: M1 is_less_or_equal_with M2 - M3 ; ::_thesis: M3 is_less_or_equal_with M2 - M1
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A4: ( len M2 = len M3 & width M2 = width M3 ) by Lm1;
A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: ( len M1 = len M2 & width M1 = width M2 ) by Lm1;
 for i, j being Nat st [i,j] in Indices M3 holds
M3 * (i,j) <= (M2 - M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M3 implies M3 * (i,j) <= (M2 - M1) * (i,j) )
assume A7: [i,j] in Indices M3 ; ::_thesis: M3 * (i,j) <= (M2 - M1) * (i,j)
then  M1 * (i,j) <= (M2 - M3) * (i,j) by A1, A2, A3, Def6;
then  M1 * (i,j) <= (M2 * (i,j)) - (M3 * (i,j)) by A5, A3, A4, A7, Th3;
then  M3 * (i,j) <= (M2 * (i,j)) - (M1 * (i,j)) by XREAL_1:11;
hence  M3 * (i,j) <= (M2 - M1) * (i,j) by A5, A3, A6, A7, Th3; ::_thesis: verum
end;
hence  M3 is_less_or_equal_with M2 - M1 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:53
for n being Nat
for M1, M2, M3 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 holds
M1 - M3 is_less_or_equal_with M2
proof
let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 holds
M1 - M3 is_less_or_equal_with M2
let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 - M2 is_less_or_equal_with M3 implies M1 - M3 is_less_or_equal_with M2 )
assume A1: M1 - M2 is_less_or_equal_with M3 ; ::_thesis: M1 - M3 is_less_or_equal_with M2
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: ( len M1 = len M3 & width M1 = width M3 ) by Lm1;
A4: Indices (M1 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: Indices (M1 - M3) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: ( len M1 = len M2 & width M1 = width M2 ) by Lm1;
 for i, j being Nat st [i,j] in Indices (M1 - M3) holds
(M1 - M3) * (i,j) <= M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M3) implies (M1 - M3) * (i,j) <= M2 * (i,j) )
assume A7: [i,j] in Indices (M1 - M3) ; ::_thesis: (M1 - M3) * (i,j) <= M2 * (i,j)
then  (M1 - M2) * (i,j) <= M3 * (i,j) by A1, A4, A5, Def6;
then  (M1 * (i,j)) - (M2 * (i,j)) <= M3 * (i,j) by A2, A5, A6, A7, Th3;
then  (M1 * (i,j)) - (M3 * (i,j)) <= M2 * (i,j) by XREAL_1:12;
hence  (M1 - M3) * (i,j) <= M2 * (i,j) by A2, A5, A3, A7, Th3; ::_thesis: verum
end;
hence  M1 - M3 is_less_or_equal_with M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:54
for n being Nat
for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_than M2 & M3 is_less_or_equal_with M4 holds
M1 - M4 is_less_than M2 - M3
proof
let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_than M2 & M3 is_less_or_equal_with M4 holds
M1 - M4 is_less_than M2 - M3
let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 & M3 is_less_or_equal_with M4 implies M1 - M4 is_less_than M2 - M3 )
assume A1: ( M1 is_less_than M2 & M3 is_less_or_equal_with M4 ) ; ::_thesis: M1 - M4 is_less_than M2 - M3
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: ( Indices M2 = [:(Seg n),(Seg n):] & len M2 = len M3 ) by Lm1, MATRIX_1:24;
A4: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: width M2 = width M3 by Lm1;
A6: Indices (M1 - M4) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A7: ( len M1 = len M4 & width M1 = width M4 ) by Lm1;
 for i, j being Nat st [i,j] in Indices (M1 - M4) holds
(M1 - M4) * (i,j) < (M2 - M3) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M4) implies (M1 - M4) * (i,j) < (M2 - M3) * (i,j) )
assume A8: [i,j] in Indices (M1 - M4) ; ::_thesis: (M1 - M4) * (i,j) < (M2 - M3) * (i,j)
then  ( M1 * (i,j) < M2 * (i,j) & M3 * (i,j) <= M4 * (i,j) ) by A1, A2, A4, A6, Def5, Def6;
then  (M1 * (i,j)) - (M4 * (i,j)) < (M2 * (i,j)) - (M3 * (i,j)) by XREAL_1:14;
then  (M1 - M4) * (i,j) < (M2 * (i,j)) - (M3 * (i,j)) by A2, A6, A7, A8, Th3;
hence  (M1 - M4) * (i,j) < (M2 - M3) * (i,j) by A6, A3, A5, A8, Th3; ::_thesis: verum
end;
hence  M1 - M4 is_less_than M2 - M3 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:55
for n being Nat
for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & M3 is_less_than M4 holds
M1 - M4 is_less_than M2 - M3
proof
let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & M3 is_less_than M4 holds
M1 - M4 is_less_than M2 - M3
let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 & M3 is_less_than M4 implies M1 - M4 is_less_than M2 - M3 )
assume A1: ( M1 is_less_or_equal_with M2 & M3 is_less_than M4 ) ; ::_thesis: M1 - M4 is_less_than M2 - M3
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: ( Indices M2 = [:(Seg n),(Seg n):] & len M2 = len M3 ) by Lm1, MATRIX_1:24;
A4: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: width M2 = width M3 by Lm1;
A6: Indices (M1 - M4) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A7: ( len M1 = len M4 & width M1 = width M4 ) by Lm1;
 for i, j being Nat st [i,j] in Indices (M1 - M4) holds
(M1 - M4) * (i,j) < (M2 - M3) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M4) implies (M1 - M4) * (i,j) < (M2 - M3) * (i,j) )
assume A8: [i,j] in Indices (M1 - M4) ; ::_thesis: (M1 - M4) * (i,j) < (M2 - M3) * (i,j)
then  ( M1 * (i,j) <= M2 * (i,j) & M3 * (i,j) < M4 * (i,j) ) by A1, A2, A4, A6, Def5, Def6;
then  (M1 * (i,j)) - (M4 * (i,j)) < (M2 * (i,j)) - (M3 * (i,j)) by XREAL_1:15;
then  (M1 - M4) * (i,j) < (M2 * (i,j)) - (M3 * (i,j)) by A2, A6, A7, A8, Th3;
hence  (M1 - M4) * (i,j) < (M2 - M3) * (i,j) by A6, A3, A5, A8, Th3; ::_thesis: verum
end;
hence  M1 - M4 is_less_than M2 - M3 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:56
for n being Nat
for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds
M1 - M3 is_less_or_equal_with M2 - M4
proof
let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds
M1 - M3 is_less_or_equal_with M2 - M4
let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 - M2 is_less_or_equal_with M3 - M4 implies M1 - M3 is_less_or_equal_with M2 - M4 )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: Indices (M1 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices (M1 - M3) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A4: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: ( len M1 = len M2 & width M1 = width M2 ) by Lm1;
A7: ( len M1 = len M3 & width M1 = width M3 ) by Lm1;
A8: ( len M3 = len M4 & width M3 = width M4 ) by Lm1;
assume A9: M1 - M2 is_less_or_equal_with M3 - M4 ; ::_thesis: M1 - M3 is_less_or_equal_with M2 - M4
 for i, j being Nat st [i,j] in Indices (M1 - M3) holds
(M1 - M3) * (i,j) <= (M2 - M4) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M3) implies (M1 - M3) * (i,j) <= (M2 - M4) * (i,j) )
assume A10: [i,j] in Indices (M1 - M3) ; ::_thesis: (M1 - M3) * (i,j) <= (M2 - M4) * (i,j)
then  (M1 - M2) * (i,j) <= (M3 - M4) * (i,j) by A9, A2, A3, Def6;
then  (M1 * (i,j)) - (M2 * (i,j)) <= (M3 - M4) * (i,j) by A1, A3, A6, A10, Th3;
then  (M1 * (i,j)) - (M2 * (i,j)) <= (M3 * (i,j)) - (M4 * (i,j)) by A4, A3, A8, A10, Th3;
then  (M1 * (i,j)) - (M3 * (i,j)) <= (M2 * (i,j)) - (M4 * (i,j)) by XREAL_1:16;
then  (M1 - M3) * (i,j) <= (M2 * (i,j)) - (M4 * (i,j)) by A1, A3, A7, A10, Th3;
hence  (M1 - M3) * (i,j) <= (M2 - M4) * (i,j) by A5, A3, A6, A8, A7, A10, Th3; ::_thesis: verum
end;
hence  M1 - M3 is_less_or_equal_with M2 - M4 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:57
for n being Nat
for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds
M4 - M2 is_less_or_equal_with M3 - M1
proof
let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds
M4 - M2 is_less_or_equal_with M3 - M1
let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 - M2 is_less_or_equal_with M3 - M4 implies M4 - M2 is_less_or_equal_with M3 - M1 )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices (M1 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A4: Indices M4 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: Indices (M4 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: ( len M1 = len M3 & width M1 = width M3 ) by Lm1;
A7: ( len M3 = len M4 & width M3 = width M4 ) by Lm1;
A8: ( len M1 = len M2 & width M1 = width M2 ) by Lm1;
assume A9: M1 - M2 is_less_or_equal_with M3 - M4 ; ::_thesis: M4 - M2 is_less_or_equal_with M3 - M1
 for i, j being Nat st [i,j] in Indices (M4 - M2) holds
(M4 - M2) * (i,j) <= (M3 - M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M4 - M2) implies (M4 - M2) * (i,j) <= (M3 - M1) * (i,j) )
assume A10: [i,j] in Indices (M4 - M2) ; ::_thesis: (M4 - M2) * (i,j) <= (M3 - M1) * (i,j)
then  (M1 - M2) * (i,j) <= (M3 - M4) * (i,j) by A9, A3, A5, Def6;
then  (M1 * (i,j)) - (M2 * (i,j)) <= (M3 - M4) * (i,j) by A1, A5, A8, A10, Th3;
then  (M1 * (i,j)) - (M2 * (i,j)) <= (M3 * (i,j)) - (M4 * (i,j)) by A2, A5, A7, A10, Th3;
then  (M4 * (i,j)) - (M2 * (i,j)) <= (M3 * (i,j)) - (M1 * (i,j)) by XREAL_1:17;
then  (M4 - M2) * (i,j) <= (M3 * (i,j)) - (M1 * (i,j)) by A4, A5, A8, A7, A6, A10, Th3;
hence  (M4 - M2) * (i,j) <= (M3 - M1) * (i,j) by A2, A5, A6, A10, Th3; ::_thesis: verum
end;
hence  M4 - M2 is_less_or_equal_with M3 - M1 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:58
for n being Nat
for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds
M4 - M3 is_less_or_equal_with M2 - M1
proof
let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds
M4 - M3 is_less_or_equal_with M2 - M1
let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 - M2 is_less_or_equal_with M3 - M4 implies M4 - M3 is_less_or_equal_with M2 - M1 )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices M4 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A4: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: Indices (M1 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: Indices (M4 - M3) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A7: ( len M3 = len M4 & width M3 = width M4 ) by Lm1;
A8: ( len M1 = len M2 & width M1 = width M2 ) by Lm1;
assume A9: M1 - M2 is_less_or_equal_with M3 - M4 ; ::_thesis: M4 - M3 is_less_or_equal_with M2 - M1
 for i, j being Nat st [i,j] in Indices (M4 - M3) holds
(M4 - M3) * (i,j) <= (M2 - M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M4 - M3) implies (M4 - M3) * (i,j) <= (M2 - M1) * (i,j) )
assume A10: [i,j] in Indices (M4 - M3) ; ::_thesis: (M4 - M3) * (i,j) <= (M2 - M1) * (i,j)
then  (M1 - M2) * (i,j) <= (M3 - M4) * (i,j) by A9, A5, A6, Def6;
then  (M1 * (i,j)) - (M2 * (i,j)) <= (M3 - M4) * (i,j) by A1, A6, A8, A10, Th3;
then  (M1 * (i,j)) - (M2 * (i,j)) <= (M3 * (i,j)) - (M4 * (i,j)) by A4, A6, A7, A10, Th3;
then  (M4 * (i,j)) - (M3 * (i,j)) <= (M2 * (i,j)) - (M1 * (i,j)) by XREAL_1:18;
then  (M4 - M3) * (i,j) <= (M2 * (i,j)) - (M1 * (i,j)) by A3, A6, A7, A10, Th3;
hence  (M4 - M3) * (i,j) <= (M2 - M1) * (i,j) by A2, A6, A8, A10, Th3; ::_thesis: verum
end;
hence  M4 - M3 is_less_or_equal_with M2 - M1 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:59
for n being Nat
for M1, M2, M3 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 holds
M1 is_less_or_equal_with M3 - M2
proof
let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 holds
M1 is_less_or_equal_with M3 - M2
let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 + M2 is_less_or_equal_with M3 implies M1 is_less_or_equal_with M3 - M2 )
assume A1: M1 + M2 is_less_or_equal_with M3 ; ::_thesis: M1 is_less_or_equal_with M3 - M2
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: width M2 = width M3 by Lm1;
A4: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: ( Indices M3 = [:(Seg n),(Seg n):] & len M2 = len M3 ) by Lm1, MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) <= (M3 - M2) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) <= (M3 - M2) * (i,j) )
assume A6: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) <= (M3 - M2) * (i,j)
then  (M1 + M2) * (i,j) <= M3 * (i,j) by A1, A2, A4, Def6;
then  (M1 * (i,j)) + (M2 * (i,j)) <= M3 * (i,j) by A6, MATRIXR1:25;
then  M1 * (i,j) <= (M3 * (i,j)) - (M2 * (i,j)) by XREAL_1:19;
hence  M1 * (i,j) <= (M3 - M2) * (i,j) by A2, A5, A3, A6, Th3; ::_thesis: verum
end;
hence  M1 is_less_or_equal_with M3 - M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:60
for n being Nat
for M1, M2, M3, M4 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 + M4 holds
M1 - M3 is_less_or_equal_with M4 - M2
proof
let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 + M4 holds
M1 - M3 is_less_or_equal_with M4 - M2
let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 + M2 is_less_or_equal_with M3 + M4 implies M1 - M3 is_less_or_equal_with M4 - M2 )
assume A1: M1 + M2 is_less_or_equal_with M3 + M4 ; ::_thesis: M1 - M3 is_less_or_equal_with M4 - M2
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: width M2 = width M4 by Lm1;
A4: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: ( Indices M4 = [:(Seg n),(Seg n):] & len M2 = len M4 ) by Lm1, MATRIX_1:24;
A6: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A7: Indices (M1 - M3) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A8: ( len M1 = len M3 & width M1 = width M3 ) by Lm1;
 for i, j being Nat st [i,j] in Indices (M1 - M3) holds
(M1 - M3) * (i,j) <= (M4 - M2) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M3) implies (M1 - M3) * (i,j) <= (M4 - M2) * (i,j) )
assume A9: [i,j] in Indices (M1 - M3) ; ::_thesis: (M1 - M3) * (i,j) <= (M4 - M2) * (i,j)
then  (M1 + M2) * (i,j) <= (M3 + M4) * (i,j) by A1, A4, A7, Def6;
then  (M1 * (i,j)) + (M2 * (i,j)) <= (M3 + M4) * (i,j) by A2, A7, A9, MATRIXR1:25;
then  (M1 * (i,j)) + (M2 * (i,j)) <= (M3 * (i,j)) + (M4 * (i,j)) by A6, A7, A9, MATRIXR1:25;
then  (M1 * (i,j)) - (M3 * (i,j)) <= (M4 * (i,j)) - (M2 * (i,j)) by XREAL_1:21;
then  (M1 - M3) * (i,j) <= (M4 * (i,j)) - (M2 * (i,j)) by A2, A7, A8, A9, Th3;
hence  (M1 - M3) * (i,j) <= (M4 - M2) * (i,j) by A7, A5, A3, A9, Th3; ::_thesis: verum
end;
hence  M1 - M3 is_less_or_equal_with M4 - M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:61
for n being Nat
for M1, M2, M3, M4 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 - M4 holds
M1 + M4 is_less_or_equal_with M3 - M2
proof
let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 - M4 holds
M1 + M4 is_less_or_equal_with M3 - M2
let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 + M2 is_less_or_equal_with M3 - M4 implies M1 + M4 is_less_or_equal_with M3 - M2 )
assume A1: M1 + M2 is_less_or_equal_with M3 - M4 ; ::_thesis: M1 + M4 is_less_or_equal_with M3 - M2
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A4: Indices (M1 + M4) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: ( len M2 = len M3 & width M2 = width M3 ) by Lm1;
A6: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A7: ( len M3 = len M4 & width M3 = width M4 ) by Lm1;
 for i, j being Nat st [i,j] in Indices (M1 + M4) holds
(M1 + M4) * (i,j) <= (M3 - M2) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M4) implies (M1 + M4) * (i,j) <= (M3 - M2) * (i,j) )
assume A8: [i,j] in Indices (M1 + M4) ; ::_thesis: (M1 + M4) * (i,j) <= (M3 - M2) * (i,j)
then  (M1 + M2) * (i,j) <= (M3 - M4) * (i,j) by A1, A3, A4, Def6;
then  (M1 * (i,j)) + (M2 * (i,j)) <= (M3 - M4) * (i,j) by A2, A4, A8, MATRIXR1:25;
then  (M1 * (i,j)) + (M2 * (i,j)) <= (M3 * (i,j)) - (M4 * (i,j)) by A6, A4, A7, A8, Th3;
then  (M1 * (i,j)) + (M4 * (i,j)) <= (M3 * (i,j)) - (M2 * (i,j)) by XREAL_1:22;
then  (M1 + M4) * (i,j) <= (M3 * (i,j)) - (M2 * (i,j)) by A2, A4, A8, MATRIXR1:25;
hence  (M1 + M4) * (i,j) <= (M3 - M2) * (i,j) by A6, A4, A5, A8, Th3; ::_thesis: verum
end;
hence  M1 + M4 is_less_or_equal_with M3 - M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:62
for n being Nat
for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 + M4 holds
M1 - M4 is_less_or_equal_with M3 + M2
proof
let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 + M4 holds
M1 - M4 is_less_or_equal_with M3 + M2
let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 - M2 is_less_or_equal_with M3 + M4 implies M1 - M4 is_less_or_equal_with M3 + M2 )
assume A1: M1 - M2 is_less_or_equal_with M3 + M4 ; ::_thesis: M1 - M4 is_less_or_equal_with M3 + M2
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices (M1 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A4: Indices (M1 - M4) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: ( len M1 = len M2 & width M1 = width M2 ) by Lm1;
A6: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A7: ( len M1 = len M4 & width M1 = width M4 ) by Lm1;
 for i, j being Nat st [i,j] in Indices (M1 - M4) holds
(M1 - M4) * (i,j) <= (M3 + M2) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M4) implies (M1 - M4) * (i,j) <= (M3 + M2) * (i,j) )
assume A8: [i,j] in Indices (M1 - M4) ; ::_thesis: (M1 - M4) * (i,j) <= (M3 + M2) * (i,j)
then  (M1 - M2) * (i,j) <= (M3 + M4) * (i,j) by A1, A3, A4, Def6;
then  (M1 * (i,j)) - (M2 * (i,j)) <= (M3 + M4) * (i,j) by A2, A4, A5, A8, Th3;
then  (M1 * (i,j)) - (M2 * (i,j)) <= (M3 * (i,j)) + (M4 * (i,j)) by A6, A4, A8, MATRIXR1:25;
then  (M1 * (i,j)) - (M4 * (i,j)) <= (M3 * (i,j)) + (M2 * (i,j)) by XREAL_1:23;
then  (M1 - M4) * (i,j) <= (M3 * (i,j)) + (M2 * (i,j)) by A2, A4, A7, A8, Th3;
hence  (M1 - M4) * (i,j) <= (M3 + M2) * (i,j) by A6, A4, A8, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 - M4 is_less_or_equal_with M3 + M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:63
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds
- M2 is_less_or_equal_with - M1
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds
- M2 is_less_or_equal_with - M1
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 implies - M2 is_less_or_equal_with - M1 )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices (- M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume A4: M1 is_less_or_equal_with M2 ; ::_thesis: - M2 is_less_or_equal_with - M1
 for i, j being Nat st [i,j] in Indices (- M2) holds
(- M2) * (i,j) <= (- M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M2) implies (- M2) * (i,j) <= (- M1) * (i,j) )
assume A5: [i,j] in Indices (- M2) ; ::_thesis: (- M2) * (i,j) <= (- M1) * (i,j)
then  M1 * (i,j) <= M2 * (i,j) by A4, A1, A3, Def6;
then  - (M2 * (i,j)) <= - (M1 * (i,j)) by XREAL_1:24;
then  (- M2) * (i,j) <= - (M1 * (i,j)) by A2, A3, A5, Th2;
hence  (- M2) * (i,j) <= (- M1) * (i,j) by A1, A3, A5, Th2; ::_thesis: verum
end;
hence  - M2 is_less_or_equal_with - M1 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:64
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with - M2 holds
M2 is_less_or_equal_with - M1
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with - M2 holds
M2 is_less_or_equal_with - M1
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with - M2 implies M2 is_less_or_equal_with - M1 )
A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A2: M1 is_less_or_equal_with - M2 ; ::_thesis: M2 is_less_or_equal_with - M1
 for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) <= (- M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) <= (- M1) * (i,j) )
assume A3: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) <= (- M1) * (i,j)
then  M1 * (i,j) <= (- M2) * (i,j) by A2, A1, Def6;
then  M1 * (i,j) <= - (M2 * (i,j)) by A3, Th2;
then  M2 * (i,j) <= - (M1 * (i,j)) by XREAL_1:25;
hence  M2 * (i,j) <= (- M1) * (i,j) by A1, A3, Th2; ::_thesis: verum
end;
hence  M2 is_less_or_equal_with - M1 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:65
for n being Nat
for M2, M1 being Matrix of n, REAL st - M2 is_less_or_equal_with M1 holds
- M1 is_less_or_equal_with M2
proof
let n be Nat; ::_thesis: for M2, M1 being Matrix of n, REAL st - M2 is_less_or_equal_with M1 holds
- M1 is_less_or_equal_with M2
let M2, M1 be Matrix of n, REAL ; ::_thesis: ( - M2 is_less_or_equal_with M1 implies - M1 is_less_or_equal_with M2 )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: Indices (- M2) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A4: Indices (- M1) = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume A5: - M2 is_less_or_equal_with M1 ; ::_thesis: - M1 is_less_or_equal_with M2
 for i, j being Nat st [i,j] in Indices (- M1) holds
(- M1) * (i,j) <= M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M1) implies (- M1) * (i,j) <= M2 * (i,j) )
assume A6: [i,j] in Indices (- M1) ; ::_thesis: (- M1) * (i,j) <= M2 * (i,j)
then  (- M2) * (i,j) <= M1 * (i,j) by A5, A4, A3, Def6;
then  - (M2 * (i,j)) <= M1 * (i,j) by A2, A4, A6, Th2;
then  - (M1 * (i,j)) <= M2 * (i,j) by XREAL_1:26;
hence  (- M1) * (i,j) <= M2 * (i,j) by A1, A4, A6, Th2; ::_thesis: verum
end;
hence  - M1 is_less_or_equal_with M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:66
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Positive holds
M2 is_less_than M2 + M1
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Positive holds
M2 is_less_than M2 + M1
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive implies M2 is_less_than M2 + M1 )
A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A2: M1 is Positive ; ::_thesis: M2 is_less_than M2 + M1
 for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) < (M2 + M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) < (M2 + M1) * (i,j) )
assume A3: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) < (M2 + M1) * (i,j)
then  M1 * (i,j) > 0 by A2, A1, Def1;
then  M2 * (i,j) < (M2 * (i,j)) + (M1 * (i,j)) by XREAL_1:29;
hence  M2 * (i,j) < (M2 + M1) * (i,j) by A3, MATRIXR1:25; ::_thesis: verum
end;
hence  M2 is_less_than M2 + M1 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:67
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Negative holds
M1 + M2 is_less_than M2
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Negative holds
M1 + M2 is_less_than M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Negative implies M1 + M2 is_less_than M2 )
A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 + M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A2: M1 is Negative ; ::_thesis: M1 + M2 is_less_than M2
 for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) < M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) < M2 * (i,j) )
assume A3: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) < M2 * (i,j)
then  M1 * (i,j) < 0 by A2, A1, Def2;
then  (M1 * (i,j)) + (M2 * (i,j)) < M2 * (i,j) by XREAL_1:30;
hence  (M1 + M2) * (i,j) < M2 * (i,j) by A1, A3, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 + M2 is_less_than M2 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:68
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Nonnegative holds
M2 is_less_or_equal_with M1 + M2
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Nonnegative holds
M2 is_less_or_equal_with M1 + M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonnegative implies M2 is_less_or_equal_with M1 + M2 )
A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A2: M1 is Nonnegative ; ::_thesis: M2 is_less_or_equal_with M1 + M2
 for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) <= (M1 + M2) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) <= (M1 + M2) * (i,j) )
assume A3: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) <= (M1 + M2) * (i,j)
then  M1 * (i,j) >= 0 by A2, A1, Def4;
then  M2 * (i,j) <= (M1 * (i,j)) + (M2 * (i,j)) by XREAL_1:31;
hence  M2 * (i,j) <= (M1 + M2) * (i,j) by A1, A3, MATRIXR1:25; ::_thesis: verum
end;
hence  M2 is_less_or_equal_with M1 + M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:69
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Nonpositive holds
M1 + M2 is_less_or_equal_with M2
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Nonpositive holds
M1 + M2 is_less_or_equal_with M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonpositive implies M1 + M2 is_less_or_equal_with M2 )
A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 + M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A2: M1 is Nonpositive ; ::_thesis: M1 + M2 is_less_or_equal_with M2
 for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * (i,j) <= M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) <= M2 * (i,j) )
assume A3: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) <= M2 * (i,j)
then  M1 * (i,j) <= 0 by A2, A1, Def3;
then  (M1 * (i,j)) + (M2 * (i,j)) <= M2 * (i,j) by XREAL_1:32;
hence  (M1 + M2) * (i,j) <= M2 * (i,j) by A1, A3, MATRIXR1:25; ::_thesis: verum
end;
hence  M1 + M2 is_less_or_equal_with M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:70
for n being Nat
for M1, M3, M2 being Matrix of n, REAL st M1 is Nonpositive & M3 is_less_or_equal_with M2 holds
M3 + M1 is_less_or_equal_with M2
proof
let n be Nat; ::_thesis: for M1, M3, M2 being Matrix of n, REAL st M1 is Nonpositive & M3 is_less_or_equal_with M2 holds
M3 + M1 is_less_or_equal_with M2
let M1, M3, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonpositive & M3 is_less_or_equal_with M2 implies M3 + M1 is_less_or_equal_with M2 )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: ( Indices M3 = [:(Seg n),(Seg n):] & Indices (M3 + M1) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A3: ( M1 is Nonpositive & M3 is_less_or_equal_with M2 ) ; ::_thesis: M3 + M1 is_less_or_equal_with M2
 for i, j being Nat st [i,j] in Indices (M3 + M1) holds
(M3 + M1) * (i,j) <= M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M3 + M1) implies (M3 + M1) * (i,j) <= M2 * (i,j) )
assume A4: [i,j] in Indices (M3 + M1) ; ::_thesis: (M3 + M1) * (i,j) <= M2 * (i,j)
then  ( M1 * (i,j) <= 0 & M3 * (i,j) <= M2 * (i,j) ) by A3, A1, A2, Def3, Def6;
then  (M3 * (i,j)) + (M1 * (i,j)) <= M2 * (i,j) by XREAL_1:35;
hence  (M3 + M1) * (i,j) <= M2 * (i,j) by A2, A4, MATRIXR1:25; ::_thesis: verum
end;
hence  M3 + M1 is_less_or_equal_with M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:71
for n being Nat
for M1, M3, M2 being Matrix of n, REAL st M1 is Nonpositive & M3 is_less_than M2 holds
M3 + M1 is_less_than M2
proof
let n be Nat; ::_thesis: for M1, M3, M2 being Matrix of n, REAL st M1 is Nonpositive & M3 is_less_than M2 holds
M3 + M1 is_less_than M2
let M1, M3, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonpositive & M3 is_less_than M2 implies M3 + M1 is_less_than M2 )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: ( Indices M3 = [:(Seg n),(Seg n):] & Indices (M3 + M1) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A3: ( M1 is Nonpositive & M3 is_less_than M2 ) ; ::_thesis: M3 + M1 is_less_than M2
 for i, j being Nat st [i,j] in Indices (M3 + M1) holds
(M3 + M1) * (i,j) < M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M3 + M1) implies (M3 + M1) * (i,j) < M2 * (i,j) )
assume A4: [i,j] in Indices (M3 + M1) ; ::_thesis: (M3 + M1) * (i,j) < M2 * (i,j)
then  ( M1 * (i,j) <= 0 & M3 * (i,j) < M2 * (i,j) ) by A3, A1, A2, Def3, Def5;
then  (M3 * (i,j)) + (M1 * (i,j)) < M2 * (i,j) by XREAL_1:36;
hence  (M3 + M1) * (i,j) < M2 * (i,j) by A2, A4, MATRIXR1:25; ::_thesis: verum
end;
hence  M3 + M1 is_less_than M2 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:72
for n being Nat
for M1, M3, M2 being Matrix of n, REAL st M1 is Negative & M3 is_less_or_equal_with M2 holds
M3 + M1 is_less_than M2
proof
let n be Nat; ::_thesis: for M1, M3, M2 being Matrix of n, REAL st M1 is Negative & M3 is_less_or_equal_with M2 holds
M3 + M1 is_less_than M2
let M1, M3, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Negative & M3 is_less_or_equal_with M2 implies M3 + M1 is_less_than M2 )
A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A2: ( Indices M3 = [:(Seg n),(Seg n):] & Indices (M3 + M1) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A3: ( M1 is Negative & M3 is_less_or_equal_with M2 ) ; ::_thesis: M3 + M1 is_less_than M2
 for i, j being Nat st [i,j] in Indices (M3 + M1) holds
(M3 + M1) * (i,j) < M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M3 + M1) implies (M3 + M1) * (i,j) < M2 * (i,j) )
assume A4: [i,j] in Indices (M3 + M1) ; ::_thesis: (M3 + M1) * (i,j) < M2 * (i,j)
then  ( M1 * (i,j) < 0 & M3 * (i,j) <= M2 * (i,j) ) by A3, A1, A2, Def2, Def6;
then  (M3 * (i,j)) + (M1 * (i,j)) < M2 * (i,j) by XREAL_1:37;
hence  (M3 + M1) * (i,j) < M2 * (i,j) by A2, A4, MATRIXR1:25; ::_thesis: verum
end;
hence  M3 + M1 is_less_than M2 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:73
for n being Nat
for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_or_equal_with M3 holds
M2 is_less_or_equal_with M1 + M3
proof
let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_or_equal_with M3 holds
M2 is_less_or_equal_with M1 + M3
let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonnegative & M2 is_less_or_equal_with M3 implies M2 is_less_or_equal_with M1 + M3 )
A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A2: ( M1 is Nonnegative & M2 is_less_or_equal_with M3 ) ; ::_thesis: M2 is_less_or_equal_with M1 + M3
 for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) <= (M1 + M3) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) <= (M1 + M3) * (i,j) )
assume A3: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) <= (M1 + M3) * (i,j)
then  ( M1 * (i,j) >= 0 & M2 * (i,j) <= M3 * (i,j) ) by A2, A1, Def4, Def6;
then  M2 * (i,j) <= (M1 * (i,j)) + (M3 * (i,j)) by XREAL_1:38;
hence  M2 * (i,j) <= (M1 + M3) * (i,j) by A1, A3, MATRIXR1:25; ::_thesis: verum
end;
hence  M2 is_less_or_equal_with M1 + M3 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:74
for n being Nat
for M1, M2, M3 being Matrix of n, REAL st M1 is Positive & M2 is_less_or_equal_with M3 holds
M2 is_less_than M1 + M3
proof
let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is Positive & M2 is_less_or_equal_with M3 holds
M2 is_less_than M1 + M3
let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive & M2 is_less_or_equal_with M3 implies M2 is_less_than M1 + M3 )
A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A2: ( M1 is Positive & M2 is_less_or_equal_with M3 ) ; ::_thesis: M2 is_less_than M1 + M3
 for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) < (M1 + M3) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) < (M1 + M3) * (i,j) )
assume A3: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) < (M1 + M3) * (i,j)
then  ( M1 * (i,j) > 0 & M2 * (i,j) <= M3 * (i,j) ) by A2, A1, Def1, Def6;
then  M2 * (i,j) < (M1 * (i,j)) + (M3 * (i,j)) by XREAL_1:39;
hence  M2 * (i,j) < (M1 + M3) * (i,j) by A1, A3, MATRIXR1:25; ::_thesis: verum
end;
hence  M2 is_less_than M1 + M3 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:75
for n being Nat
for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_than M3 holds
M2 is_less_than M1 + M3
proof
let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_than M3 holds
M2 is_less_than M1 + M3
let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonnegative & M2 is_less_than M3 implies M2 is_less_than M1 + M3 )
A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
assume A2: ( M1 is Nonnegative & M2 is_less_than M3 ) ; ::_thesis: M2 is_less_than M1 + M3
 for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) < (M1 + M3) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) < (M1 + M3) * (i,j) )
assume A3: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) < (M1 + M3) * (i,j)
then  ( M1 * (i,j) >= 0 & M2 * (i,j) < M3 * (i,j) ) by A2, A1, Def4, Def5;
then  M2 * (i,j) < (M1 * (i,j)) + (M3 * (i,j)) by XREAL_1:40;
hence  M2 * (i,j) < (M1 + M3) * (i,j) by A1, A3, MATRIXR1:25; ::_thesis: verum
end;
hence  M2 is_less_than M1 + M3 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:76
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Nonnegative holds
M2 - M1 is_less_or_equal_with M2
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Nonnegative holds
M2 - M1 is_less_or_equal_with M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonnegative implies M2 - M1 is_less_or_equal_with M2 )
assume A1: M1 is Nonnegative ; ::_thesis: M2 - M1 is_less_or_equal_with M2
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: width M1 = width M2 by Lm1;
A4: Indices (M2 - M1) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: ( Indices M2 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (M2 - M1) holds
(M2 - M1) * (i,j) <= M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M2 - M1) implies (M2 - M1) * (i,j) <= M2 * (i,j) )
assume A6: [i,j] in Indices (M2 - M1) ; ::_thesis: (M2 - M1) * (i,j) <= M2 * (i,j)
then  M1 * (i,j) >= 0 by A1, A2, A4, Def4;
then  (M2 * (i,j)) - (M1 * (i,j)) <= M2 * (i,j) by XREAL_1:43;
hence  (M2 - M1) * (i,j) <= M2 * (i,j) by A4, A5, A3, A6, Th3; ::_thesis: verum
end;
hence  M2 - M1 is_less_or_equal_with M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:77
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Positive holds
M2 - M1 is_less_than M2
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Positive holds
M2 - M1 is_less_than M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive implies M2 - M1 is_less_than M2 )
assume A1: M1 is Positive ; ::_thesis: M2 - M1 is_less_than M2
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: width M1 = width M2 by Lm1;
A4: Indices (M2 - M1) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: ( Indices M2 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (M2 - M1) holds
(M2 - M1) * (i,j) < M2 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M2 - M1) implies (M2 - M1) * (i,j) < M2 * (i,j) )
assume A6: [i,j] in Indices (M2 - M1) ; ::_thesis: (M2 - M1) * (i,j) < M2 * (i,j)
then  M1 * (i,j) > 0 by A1, A2, A4, Def1;
then  (M2 * (i,j)) - (M1 * (i,j)) < M2 * (i,j) by XREAL_1:44;
hence  (M2 - M1) * (i,j) < M2 * (i,j) by A4, A5, A3, A6, Th3; ::_thesis: verum
end;
hence  M2 - M1 is_less_than M2 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:78
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Nonpositive holds
M2 is_less_or_equal_with M2 - M1
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Nonpositive holds
M2 is_less_or_equal_with M2 - M1
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonpositive implies M2 is_less_or_equal_with M2 - M1 )
assume A1: M1 is Nonpositive ; ::_thesis: M2 is_less_or_equal_with M2 - M1
A2: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
A3: ( len M1 = len M2 & width M1 = width M2 ) by Lm1;
 for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) <= (M2 - M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) <= (M2 - M1) * (i,j) )
assume A4: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) <= (M2 - M1) * (i,j)
then  M1 * (i,j) <= 0 by A1, A2, Def3;
then  M2 * (i,j) <= (M2 * (i,j)) - (M1 * (i,j)) by XREAL_1:45;
hence  M2 * (i,j) <= (M2 - M1) * (i,j) by A3, A4, Th3; ::_thesis: verum
end;
hence  M2 is_less_or_equal_with M2 - M1 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:79
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is Negative holds
M2 is_less_than M2 - M1
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Negative holds
M2 is_less_than M2 - M1
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Negative implies M2 is_less_than M2 - M1 )
assume A1: M1 is Negative ; ::_thesis: M2 is_less_than M2 - M1
A2: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
A3: ( len M1 = len M2 & width M1 = width M2 ) by Lm1;
 for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) < (M2 - M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) < (M2 - M1) * (i,j) )
assume A4: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) < (M2 - M1) * (i,j)
then  M1 * (i,j) < 0 by A1, A2, Def2;
then  M2 * (i,j) < (M2 * (i,j)) - (M1 * (i,j)) by XREAL_1:46;
hence  M2 * (i,j) < (M2 - M1) * (i,j) by A3, A4, Th3; ::_thesis: verum
end;
hence  M2 is_less_than M2 - M1 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:80
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds
M2 - M1 is Nonnegative
proof
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds
M2 - M1 is Nonnegative
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 implies M2 - M1 is Nonnegative )
assume A1: M1 is_less_or_equal_with M2 ; ::_thesis: M2 - M1 is Nonnegative
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: width M1 = width M2 by Lm1;
A4: Indices (M2 - M1) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A5: ( Indices M2 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (M2 - M1) holds
(M2 - M1) * (i,j) >= 0
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M2 - M1) implies (M2 - M1) * (i,j) >= 0 )
assume A6: [i,j] in Indices (M2 - M1) ; ::_thesis: (M2 - M1) * (i,j) >= 0
then  M1 * (i,j) <= M2 * (i,j) by A1, A2, A4, Def6;
then  (M2 * (i,j)) - (M1 * (i,j)) >= 0 by XREAL_1:48;
hence  (M2 - M1) * (i,j) >= 0 by A4, A5, A3, A6, Th3; ::_thesis: verum
end;
hence  M2 - M1 is Nonnegative by Def4; ::_thesis: verum
end;

theorem :: MATRIX10:81
for n being Nat
for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_than M3 holds
M2 - M1 is_less_than M3
proof
let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_than M3 holds
M2 - M1 is_less_than M3
let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonnegative & M2 is_less_than M3 implies M2 - M1 is_less_than M3 )
assume A1: ( M1 is Nonnegative & M2 is_less_than M3 ) ; ::_thesis: M2 - M1 is_less_than M3
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: ( Indices M2 = [:(Seg n),(Seg n):] & Indices (M2 - M1) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
A4: ( len M1 = len M2 & width M1 = width M2 ) by Lm1;
 for i, j being Nat st [i,j] in Indices (M2 - M1) holds
(M2 - M1) * (i,j) < M3 * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (M2 - M1) implies (M2 - M1) * (i,j) < M3 * (i,j) )
assume A5: [i,j] in Indices (M2 - M1) ; ::_thesis: (M2 - M1) * (i,j) < M3 * (i,j)
then  ( M1 * (i,j) >= 0 & M2 * (i,j) < M3 * (i,j) ) by A1, A2, A3, Def4, Def5;
then  (M2 * (i,j)) - (M1 * (i,j)) < M3 * (i,j) by XREAL_1:51;
hence  (M2 - M1) * (i,j) < M3 * (i,j) by A3, A4, A5, Th3; ::_thesis: verum
end;
hence  M2 - M1 is_less_than M3 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:82
for n being Nat
for M1, M2, M3 being Matrix of n, REAL st M1 is Nonpositive & M2 is_less_or_equal_with M3 holds
M2 is_less_or_equal_with M3 - M1
proof
let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is Nonpositive & M2 is_less_or_equal_with M3 holds
M2 is_less_or_equal_with M3 - M1
let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonpositive & M2 is_less_or_equal_with M3 implies M2 is_less_or_equal_with M3 - M1 )
assume A1: ( M1 is Nonpositive & M2 is_less_or_equal_with M3 ) ; ::_thesis: M2 is_less_or_equal_with M3 - M1
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: width M2 = width M3 by Lm1;
A4: ( width M1 = width M2 & len M2 = len M3 ) by Lm1;
A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: ( Indices M3 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) <= (M3 - M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) <= (M3 - M1) * (i,j) )
assume A7: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) <= (M3 - M1) * (i,j)
then  ( M1 * (i,j) <= 0 & M2 * (i,j) <= M3 * (i,j) ) by A1, A2, A5, Def3, Def6;
then  M2 * (i,j) <= (M3 * (i,j)) - (M1 * (i,j)) by XREAL_1:52;
hence  M2 * (i,j) <= (M3 - M1) * (i,j) by A5, A6, A4, A3, A7, Th3; ::_thesis: verum
end;
hence  M2 is_less_or_equal_with M3 - M1 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:83
for n being Nat
for M1, M2, M3 being Matrix of n, REAL st M1 is Nonpositive & M2 is_less_than M3 holds
M2 is_less_than M3 - M1
proof
let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is Nonpositive & M2 is_less_than M3 holds
M2 is_less_than M3 - M1
let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonpositive & M2 is_less_than M3 implies M2 is_less_than M3 - M1 )
assume A1: ( M1 is Nonpositive & M2 is_less_than M3 ) ; ::_thesis: M2 is_less_than M3 - M1
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: width M2 = width M3 by Lm1;
A4: ( width M1 = width M2 & len M2 = len M3 ) by Lm1;
A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: ( Indices M3 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) < (M3 - M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) < (M3 - M1) * (i,j) )
assume A7: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) < (M3 - M1) * (i,j)
then  ( M1 * (i,j) <= 0 & M2 * (i,j) < M3 * (i,j) ) by A1, A2, A5, Def3, Def5;
then  M2 * (i,j) < (M3 * (i,j)) - (M1 * (i,j)) by XREAL_1:53;
hence  M2 * (i,j) < (M3 - M1) * (i,j) by A5, A6, A4, A3, A7, Th3; ::_thesis: verum
end;
hence  M2 is_less_than M3 - M1 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:84
for n being Nat
for M1, M2, M3 being Matrix of n, REAL st M1 is Negative & M2 is_less_or_equal_with M3 holds
M2 is_less_than M3 - M1
proof
let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is Negative & M2 is_less_or_equal_with M3 holds
M2 is_less_than M3 - M1
let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is Negative & M2 is_less_or_equal_with M3 implies M2 is_less_than M3 - M1 )
assume A1: ( M1 is Negative & M2 is_less_or_equal_with M3 ) ; ::_thesis: M2 is_less_than M3 - M1
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: width M2 = width M3 by Lm1;
A4: ( width M1 = width M2 & len M2 = len M3 ) by Lm1;
A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A6: ( Indices M3 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) < (M3 - M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) < (M3 - M1) * (i,j) )
assume A7: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) < (M3 - M1) * (i,j)
then  ( M1 * (i,j) < 0 & M2 * (i,j) <= M3 * (i,j) ) by A1, A2, A5, Def2, Def6;
then  M2 * (i,j) < (M3 * (i,j)) - (M1 * (i,j)) by XREAL_1:54;
hence  M2 * (i,j) < (M3 - M1) * (i,j) by A5, A6, A4, A3, A7, Th3; ::_thesis: verum
end;
hence  M2 is_less_than M3 - M1 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:85
for a being Element of REAL
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a > 0 holds
a * M1 is_less_than a * M2
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a > 0 holds
a * M1 is_less_than a * M2
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a > 0 holds
a * M1 is_less_than a * M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 & a > 0 implies a * M1 is_less_than a * M2 )
assume that
A1: M1 is_less_than M2 and
A2: a > 0 ; ::_thesis: a * M1 is_less_than a * M2
A3: Indices (a * M1) = Indices M1 by MATRIXR1:28;
A4: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) < (a * M2) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) < (a * M2) * (i,j) )
assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) < (a * M2) * (i,j)
then  M1 * (i,j) < M2 * (i,j) by A1, A3, Def5;
then  a * (M1 * (i,j)) < a * (M2 * (i,j)) by A2, XREAL_1:68;
then A6: (a * M1) * (i,j) < a * (M2 * (i,j)) by A3, A5, Th4;
 [i,j] in Indices M2 by A4, A5, MATRIX_1:24;
hence  (a * M1) * (i,j) < (a * M2) * (i,j) by A6, Th4; ::_thesis: verum
end;
hence  a * M1 is_less_than a * M2 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:86
for a being Element of REAL
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a >= 0 holds
a * M1 is_less_or_equal_with a * M2
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a >= 0 holds
a * M1 is_less_or_equal_with a * M2
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a >= 0 holds
a * M1 is_less_or_equal_with a * M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 & a >= 0 implies a * M1 is_less_or_equal_with a * M2 )
assume that
A1: M1 is_less_than M2 and
A2: a >= 0 ; ::_thesis: a * M1 is_less_or_equal_with a * M2
A3: Indices (a * M1) = Indices M1 by MATRIXR1:28;
A4: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) <= (a * M2) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) <= (a * M2) * (i,j) )
assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) <= (a * M2) * (i,j)
then  M1 * (i,j) < M2 * (i,j) by A1, A3, Def5;
then  a * (M1 * (i,j)) <= a * (M2 * (i,j)) by A2, XREAL_1:64;
then A6: (a * M1) * (i,j) <= a * (M2 * (i,j)) by A3, A5, Th4;
 [i,j] in Indices M2 by A4, A5, MATRIX_1:24;
hence  (a * M1) * (i,j) <= (a * M2) * (i,j) by A6, Th4; ::_thesis: verum
end;
hence  a * M1 is_less_or_equal_with a * M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:87
for a being Element of REAL
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a < 0 holds
a * M2 is_less_than a * M1
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a < 0 holds
a * M2 is_less_than a * M1
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a < 0 holds
a * M2 is_less_than a * M1
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 & a < 0 implies a * M2 is_less_than a * M1 )
assume that
A1: M1 is_less_than M2 and
A2: a < 0 ; ::_thesis: a * M2 is_less_than a * M1
A3: Indices (a * M2) = Indices M2 by MATRIXR1:28;
A4: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (a * M2) holds
(a * M2) * (i,j) < (a * M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M2) implies (a * M2) * (i,j) < (a * M1) * (i,j) )
assume A5: [i,j] in Indices (a * M2) ; ::_thesis: (a * M2) * (i,j) < (a * M1) * (i,j)
then A6: [i,j] in Indices M1 by A4, MATRIX_1:24;
then  M1 * (i,j) < M2 * (i,j) by A1, Def5;
then  a * (M2 * (i,j)) < a * (M1 * (i,j)) by A2, XREAL_1:69;
then  (a * M2) * (i,j) < a * (M1 * (i,j)) by A3, A5, Th4;
hence  (a * M2) * (i,j) < (a * M1) * (i,j) by A6, Th4; ::_thesis: verum
end;
hence  a * M2 is_less_than a * M1 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:88
for a being Element of REAL
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a <= 0 holds
a * M2 is_less_or_equal_with a * M1
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a <= 0 holds
a * M2 is_less_or_equal_with a * M1
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a <= 0 holds
a * M2 is_less_or_equal_with a * M1
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 & a <= 0 implies a * M2 is_less_or_equal_with a * M1 )
assume that
A1: M1 is_less_than M2 and
A2: a <= 0 ; ::_thesis: a * M2 is_less_or_equal_with a * M1
A3: Indices (a * M2) = Indices M2 by MATRIXR1:28;
A4: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (a * M2) holds
(a * M2) * (i,j) <= (a * M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M2) implies (a * M2) * (i,j) <= (a * M1) * (i,j) )
assume A5: [i,j] in Indices (a * M2) ; ::_thesis: (a * M2) * (i,j) <= (a * M1) * (i,j)
then A6: [i,j] in Indices M1 by A4, MATRIX_1:24;
then  M1 * (i,j) < M2 * (i,j) by A1, Def5;
then  a * (M2 * (i,j)) <= a * (M1 * (i,j)) by A2, XREAL_1:65;
then  (a * M2) * (i,j) <= a * (M1 * (i,j)) by A3, A5, Th4;
hence  (a * M2) * (i,j) <= (a * M1) * (i,j) by A6, Th4; ::_thesis: verum
end;
hence  a * M2 is_less_or_equal_with a * M1 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:89
for a being Element of REAL
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & a >= 0 holds
a * M1 is_less_or_equal_with a * M2
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & a >= 0 holds
a * M1 is_less_or_equal_with a * M2
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & a >= 0 holds
a * M1 is_less_or_equal_with a * M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 & a >= 0 implies a * M1 is_less_or_equal_with a * M2 )
assume that
A1: M1 is_less_or_equal_with M2 and
A2: a >= 0 ; ::_thesis: a * M1 is_less_or_equal_with a * M2
A3: Indices (a * M1) = Indices M1 by MATRIXR1:28;
A4: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) <= (a * M2) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) <= (a * M2) * (i,j) )
assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) <= (a * M2) * (i,j)
then  M1 * (i,j) <= M2 * (i,j) by A1, A3, Def6;
then  a * (M1 * (i,j)) <= a * (M2 * (i,j)) by A2, XREAL_1:64;
then A6: (a * M1) * (i,j) <= a * (M2 * (i,j)) by A3, A5, Th4;
 [i,j] in Indices M2 by A4, A5, MATRIX_1:24;
hence  (a * M1) * (i,j) <= (a * M2) * (i,j) by A6, Th4; ::_thesis: verum
end;
hence  a * M1 is_less_or_equal_with a * M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:90
for a being Element of REAL
for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & a <= 0 holds
a * M2 is_less_or_equal_with a * M1
proof
let a be Element of REAL ; ::_thesis: for n being Nat
for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & a <= 0 holds
a * M2 is_less_or_equal_with a * M1
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & a <= 0 holds
a * M2 is_less_or_equal_with a * M1
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 & a <= 0 implies a * M2 is_less_or_equal_with a * M1 )
assume that
A1: M1 is_less_or_equal_with M2 and
A2: a <= 0 ; ::_thesis: a * M2 is_less_or_equal_with a * M1
A3: Indices (a * M2) = Indices M2 by MATRIXR1:28;
A4: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (a * M2) holds
(a * M2) * (i,j) <= (a * M1) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M2) implies (a * M2) * (i,j) <= (a * M1) * (i,j) )
assume A5: [i,j] in Indices (a * M2) ; ::_thesis: (a * M2) * (i,j) <= (a * M1) * (i,j)
then A6: [i,j] in Indices M1 by A4, MATRIX_1:24;
then  M1 * (i,j) <= M2 * (i,j) by A1, Def6;
then  a * (M2 * (i,j)) <= a * (M1 * (i,j)) by A2, XREAL_1:65;
then  (a * M2) * (i,j) <= a * (M1 * (i,j)) by A3, A5, Th4;
hence  (a * M2) * (i,j) <= (a * M1) * (i,j) by A6, Th4; ::_thesis: verum
end;
hence  a * M2 is_less_or_equal_with a * M1 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:91
for a, b being Element of REAL
for n being Nat
for M1, M2 being Matrix of n, REAL st a >= 0 & a <= b & M1 is Nonnegative & M1 is_less_or_equal_with M2 holds
a * M1 is_less_or_equal_with b * M2
proof
let a, b be Element of REAL ; ::_thesis: for n being Nat
for M1, M2 being Matrix of n, REAL st a >= 0 & a <= b & M1 is Nonnegative & M1 is_less_or_equal_with M2 holds
a * M1 is_less_or_equal_with b * M2
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st a >= 0 & a <= b & M1 is Nonnegative & M1 is_less_or_equal_with M2 holds
a * M1 is_less_or_equal_with b * M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( a >= 0 & a <= b & M1 is Nonnegative & M1 is_less_or_equal_with M2 implies a * M1 is_less_or_equal_with b * M2 )
assume that
A1: ( a >= 0 & a <= b ) and
A2: ( M1 is Nonnegative & M1 is_less_or_equal_with M2 ) ; ::_thesis: a * M1 is_less_or_equal_with b * M2
A3: Indices (a * M1) = Indices M1 by MATRIXR1:28;
A4: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) <= (b * M2) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) <= (b * M2) * (i,j) )
assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) <= (b * M2) * (i,j)
then  ( M1 * (i,j) >= 0 & M1 * (i,j) <= M2 * (i,j) ) by A2, A3, Def4, Def6;
then  a * (M1 * (i,j)) <= b * (M2 * (i,j)) by A1, XREAL_1:66;
then  (a * M1) * (i,j) <= b * (M2 * (i,j)) by A3, A5, Th4;
hence  (a * M1) * (i,j) <= (b * M2) * (i,j) by A4, A3, A5, Th4; ::_thesis: verum
end;
hence  a * M1 is_less_or_equal_with b * M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:92
for a, b being Element of REAL
for n being Nat
for M1, M2 being Matrix of n, REAL st a <= 0 & b <= a & M1 is Nonpositive & M2 is_less_or_equal_with M1 holds
a * M1 is_less_or_equal_with b * M2
proof
let a, b be Element of REAL ; ::_thesis: for n being Nat
for M1, M2 being Matrix of n, REAL st a <= 0 & b <= a & M1 is Nonpositive & M2 is_less_or_equal_with M1 holds
a * M1 is_less_or_equal_with b * M2
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st a <= 0 & b <= a & M1 is Nonpositive & M2 is_less_or_equal_with M1 holds
a * M1 is_less_or_equal_with b * M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( a <= 0 & b <= a & M1 is Nonpositive & M2 is_less_or_equal_with M1 implies a * M1 is_less_or_equal_with b * M2 )
assume that
A1: ( a <= 0 & b <= a ) and
A2: ( M1 is Nonpositive & M2 is_less_or_equal_with M1 ) ; ::_thesis: a * M1 is_less_or_equal_with b * M2
A3: Indices (a * M1) = Indices M1 by MATRIXR1:28;
A4: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) <= (b * M2) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) <= (b * M2) * (i,j) )
assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) <= (b * M2) * (i,j)
then  ( M1 * (i,j) <= 0 & M2 * (i,j) <= M1 * (i,j) ) by A2, A4, A3, Def3, Def6;
then  a * (M1 * (i,j)) <= b * (M2 * (i,j)) by A1, XREAL_1:67;
then  (a * M1) * (i,j) <= b * (M2 * (i,j)) by A3, A5, Th4;
hence  (a * M1) * (i,j) <= (b * M2) * (i,j) by A4, A3, A5, Th4; ::_thesis: verum
end;
hence  a * M1 is_less_or_equal_with b * M2 by Def6; ::_thesis: verum
end;

theorem :: MATRIX10:93
for a, b being Element of REAL
for n being Nat
for M1, M2 being Matrix of n, REAL st a < 0 & b <= a & M1 is Negative & M2 is_less_than M1 holds
a * M1 is_less_than b * M2
proof
let a, b be Element of REAL ; ::_thesis: for n being Nat
for M1, M2 being Matrix of n, REAL st a < 0 & b <= a & M1 is Negative & M2 is_less_than M1 holds
a * M1 is_less_than b * M2
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st a < 0 & b <= a & M1 is Negative & M2 is_less_than M1 holds
a * M1 is_less_than b * M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( a < 0 & b <= a & M1 is Negative & M2 is_less_than M1 implies a * M1 is_less_than b * M2 )
assume that
A1: ( a < 0 & b <= a ) and
A2: ( M1 is Negative & M2 is_less_than M1 ) ; ::_thesis: a * M1 is_less_than b * M2
A3: Indices (a * M1) = Indices M1 by MATRIXR1:28;
A4: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) < (b * M2) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) < (b * M2) * (i,j) )
assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) < (b * M2) * (i,j)
then  ( M1 * (i,j) < 0 & M2 * (i,j) < M1 * (i,j) ) by A2, A4, A3, Def2, Def5;
then  a * (M1 * (i,j)) < b * (M2 * (i,j)) by A1, XREAL_1:70;
then  (a * M1) * (i,j) < b * (M2 * (i,j)) by A3, A5, Th4;
hence  (a * M1) * (i,j) < (b * M2) * (i,j) by A4, A3, A5, Th4; ::_thesis: verum
end;
hence  a * M1 is_less_than b * M2 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:94
for a, b being Element of REAL
for n being Nat
for M1, M2 being Matrix of n, REAL st a >= 0 & a < b & M1 is Nonnegative & M1 is_less_than M2 holds
a * M1 is_less_than b * M2
proof
let a, b be Element of REAL ; ::_thesis: for n being Nat
for M1, M2 being Matrix of n, REAL st a >= 0 & a < b & M1 is Nonnegative & M1 is_less_than M2 holds
a * M1 is_less_than b * M2
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st a >= 0 & a < b & M1 is Nonnegative & M1 is_less_than M2 holds
a * M1 is_less_than b * M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( a >= 0 & a < b & M1 is Nonnegative & M1 is_less_than M2 implies a * M1 is_less_than b * M2 )
assume that
A1: ( a >= 0 & a < b ) and
A2: ( M1 is Nonnegative & M1 is_less_than M2 ) ; ::_thesis: a * M1 is_less_than b * M2
A3: Indices (a * M1) = Indices M1 by MATRIXR1:28;
A4: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) < (b * M2) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) < (b * M2) * (i,j) )
assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) < (b * M2) * (i,j)
then  ( M1 * (i,j) >= 0 & M1 * (i,j) < M2 * (i,j) ) by A2, A3, Def4, Def5;
then  a * (M1 * (i,j)) < b * (M2 * (i,j)) by A1, XREAL_1:96;
then  (a * M1) * (i,j) < b * (M2 * (i,j)) by A3, A5, Th4;
hence  (a * M1) * (i,j) < (b * M2) * (i,j) by A4, A3, A5, Th4; ::_thesis: verum
end;
hence  a * M1 is_less_than b * M2 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:95
for a, b being Element of REAL
for n being Nat
for M1, M2 being Matrix of n, REAL st a >= 0 & a < b & M1 is Positive & M1 is_less_or_equal_with M2 holds
a * M1 is_less_than b * M2
proof
let a, b be Element of REAL ; ::_thesis: for n being Nat
for M1, M2 being Matrix of n, REAL st a >= 0 & a < b & M1 is Positive & M1 is_less_or_equal_with M2 holds
a * M1 is_less_than b * M2
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st a >= 0 & a < b & M1 is Positive & M1 is_less_or_equal_with M2 holds
a * M1 is_less_than b * M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( a >= 0 & a < b & M1 is Positive & M1 is_less_or_equal_with M2 implies a * M1 is_less_than b * M2 )
assume that
A1: ( a >= 0 & a < b ) and
A2: ( M1 is Positive & M1 is_less_or_equal_with M2 ) ; ::_thesis: a * M1 is_less_than b * M2
A3: Indices (a * M1) = Indices M1 by MATRIXR1:28;
A4: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) < (b * M2) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) < (b * M2) * (i,j) )
assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) < (b * M2) * (i,j)
then  ( M1 * (i,j) > 0 & M1 * (i,j) <= M2 * (i,j) ) by A2, A3, Def1, Def6;
then  a * (M1 * (i,j)) < b * (M2 * (i,j)) by A1, XREAL_1:97;
then  (a * M1) * (i,j) < b * (M2 * (i,j)) by A3, A5, Th4;
hence  (a * M1) * (i,j) < (b * M2) * (i,j) by A4, A3, A5, Th4; ::_thesis: verum
end;
hence  a * M1 is_less_than b * M2 by Def5; ::_thesis: verum
end;

theorem :: MATRIX10:96
for a, b being Element of REAL
for n being Nat
for M1, M2 being Matrix of n, REAL st a > 0 & a <= b & M1 is Positive & M1 is_less_than M2 holds
a * M1 is_less_than b * M2
proof
let a, b be Element of REAL ; ::_thesis: for n being Nat
for M1, M2 being Matrix of n, REAL st a > 0 & a <= b & M1 is Positive & M1 is_less_than M2 holds
a * M1 is_less_than b * M2
let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st a > 0 & a <= b & M1 is Positive & M1 is_less_than M2 holds
a * M1 is_less_than b * M2
let M1, M2 be Matrix of n, REAL ; ::_thesis: ( a > 0 & a <= b & M1 is Positive & M1 is_less_than M2 implies a * M1 is_less_than b * M2 )
assume that
A1: ( a > 0 & a <= b ) and
A2: ( M1 is Positive & M1 is_less_than M2 ) ; ::_thesis: a * M1 is_less_than b * M2
A3: Indices (a * M1) = Indices M1 by MATRIXR1:28;
A4: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
 for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) < (b * M2) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) < (b * M2) * (i,j) )
assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) < (b * M2) * (i,j)
then  ( M1 * (i,j) > 0 & M1 * (i,j) < M2 * (i,j) ) by A2, A3, Def1, Def5;
then  a * (M1 * (i,j)) < b * (M2 * (i,j)) by A1, XREAL_1:98;
then  (a * M1) * (i,j) < b * (M2 * (i,j)) by A3, A5, Th4;
hence  (a * M1) * (i,j) < (b * M2) * (i,j) by A4, A3, A5, Th4; ::_thesis: verum
end;
hence  a * M1 is_less_than b * M2 by Def5; ::_thesis: verum
end;