:: MATRPROB semantic presentation

begin


definition
let d be set ;
let g be FinSequence of d * ;
let n be Nat;
:: original: .
redefine funcg . n ->  FinSequence of d;
correctness
coherence
g . n is FinSequence of d;
proof
percases ( n in dom g or not n in dom g ) ;
supposeA1: n in dom g ; ::_thesis: g . n is FinSequence of d
A2: rng g c= d * by FINSEQ_1:def_4;
 g . n in rng g by A1, FUNCT_1:3;
then  g . n is Element of d * by A2;
hence  g . n is FinSequence of d ; ::_thesis: verum
end;
suppose not n in dom g ; ::_thesis: g . n is FinSequence of d
then  g . n = <*> d by FUNCT_1:def_2;
hence  g . n is FinSequence of d ; ::_thesis: verum
end;
end;
end;
end;

definition
let x be real number ;
:: original: <*
redefine func<*x*> ->  FinSequence of REAL ;
coherence
 <*x*> is FinSequence of REAL
proof
 rng <*x*> c= REAL ;
hence  <*x*> is FinSequence of REAL by FINSEQ_1:def_4; ::_thesis: verum
end;
end;

theorem Th1: :: MATRPROB:1
for D being non empty set
for a being Element of D
for m being non empty Nat
for g being FinSequence of D holds
( ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) ) iff g = m |-> a )
proof
let D be non empty set ; ::_thesis: for a being Element of D
for m being non empty Nat
for g being FinSequence of D holds
( ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) ) iff g = m |-> a )
let a be Element of D; ::_thesis: for m being non empty Nat
for g being FinSequence of D holds
( ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) ) iff g = m |-> a )
let m be non empty Nat; ::_thesis: for g being FinSequence of D holds
( ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) ) iff g = m |-> a )
let g be FinSequence of D; ::_thesis: ( ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) ) iff g = m |-> a )
hereby  ::_thesis: ( g = m |-> a implies ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) ) )
assume that
A1: len g = m and
A2: for i being Nat st i in dom g holds
g . i = a ; ::_thesis: g = m |-> a
 ( dom g = dom (m |-> a) & ( for i being Nat st i in dom g holds
g . i = (m |-> a) . i ) )
proof
thus  dom g = Seg m by A1, FINSEQ_1:def_3
.= dom (m |-> a) by FUNCOP_1:13 ; ::_thesis: for i being Nat st i in dom g holds
g . i = (m |-> a) . i
let i be Nat; ::_thesis: ( i in dom g implies g . i = (m |-> a) . i )
assume A3: i in dom g ; ::_thesis: g . i = (m |-> a) . i
A4: i in Seg m by A1, A3, FINSEQ_1:def_3;
thus g . i = a by A2, A3
.= (m |-> a) . i by A4, FINSEQ_2:57 ; ::_thesis: verum
end;
hence  g = m |-> a by FINSEQ_1:13; ::_thesis: verum
end;
assume A5: g = m |-> a ; ::_thesis: ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) )
then  dom g = Seg m by FUNCOP_1:13;
hence  ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) ) by A5, CARD_1:def_7, FINSEQ_2:57; ::_thesis: verum
end;

theorem Th2: :: MATRPROB:2
for D being non empty set
for k being Element of NAT
for n being Nat
for a, b being Element of D ex g being FinSequence of D st
( len g = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies g . i = a ) & ( not i in Seg k implies g . i = b ) ) ) )
proof
let D be non empty set ; ::_thesis: for k being Element of NAT
for n being Nat
for a, b being Element of D ex g being FinSequence of D st
( len g = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies g . i = a ) & ( not i in Seg k implies g . i = b ) ) ) )
let k be Element of NAT ; ::_thesis: for n being Nat
for a, b being Element of D ex g being FinSequence of D st
( len g = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies g . i = a ) & ( not i in Seg k implies g . i = b ) ) ) )
let n be Nat; ::_thesis: for a, b being Element of D ex g being FinSequence of D st
( len g = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies g . i = a ) & ( not i in Seg k implies g . i = b ) ) ) )
let a, b be Element of D; ::_thesis: ex g being FinSequence of D st
( len g = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies g . i = a ) & ( not i in Seg k implies g . i = b ) ) ) )
defpred S1[ set ] means $1 in Seg k;
deffunc H1( set ) ->  Element of D = a;
deffunc H2( set ) ->  Element of D = b;
 ex f being Function st
( dom f = Seg n & ( for x being set st x in Seg n holds
( ( S1[x] implies f . x = H1(x) ) & ( not S1[x] implies f . x = H2(x) ) ) ) ) from PARTFUN1:sch_1();
then consider f being Function such that
A1: dom f = Seg n and
A2: for x being set st x in Seg n holds
( ( x in Seg k implies f . x = a ) & ( not x in Seg k implies f . x = b ) ) ;
reconsider p = f as FinSequence by A1, FINSEQ_1:def_2;
 rng p c= D
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in D )
assume  y in rng p ; ::_thesis: y in D
then consider j being set  such that
A3: j in dom p and
A4: y = p . j by FUNCT_1:def_3;
A5: ( not j in Seg k implies p . j = b ) by A1, A2, A3;
 ( j in Seg k implies p . j = a ) by A1, A2, A3;
hence  y in D by A4, A5; ::_thesis: verum
end;
then reconsider p = p as FinSequence of D by FINSEQ_1:def_4;
take  p ; ::_thesis: ( len p = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies p . i = a ) & ( not i in Seg k implies p . i = b ) ) ) )
 n in NAT by ORDINAL1:def_12;
hence  ( len p = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies p . i = a ) & ( not i in Seg k implies p . i = b ) ) ) ) by A1, A2, FINSEQ_1:def_3; ::_thesis: verum
end;

theorem Th3: :: MATRPROB:3
for e being FinSequence of REAL st ( for i being Nat st i in dom e holds
0 <= e . i ) holds
for f being Real_Sequence st ( for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) holds
for n, m being Nat st n in dom e & m in dom e & n <= m holds
f . n <= f . m
proof
let e be FinSequence of REAL ; ::_thesis: ( ( for i being Nat st i in dom e holds
0 <= e . i ) implies for f being Real_Sequence st ( for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) holds
for n, m being Nat st n in dom e & m in dom e & n <= m holds
f . n <= f . m )
assume A1: for i being Nat st i in dom e holds
0 <= e . i ; ::_thesis: for f being Real_Sequence st ( for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) holds
for n, m being Nat st n in dom e & m in dom e & n <= m holds
f . n <= f . m
let f be Real_Sequence; ::_thesis: ( ( for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) implies for n, m being Nat st n in dom e & m in dom e & n <= m holds
f . n <= f . m )
assume A2: for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ; ::_thesis: for n, m being Nat st n in dom e & m in dom e & n <= m holds
f . n <= f . m
A3: for n being Nat st n <> 0 & n < len e holds
f . n <= f . (n + 1)
proof
let n be Nat; ::_thesis: ( n <> 0 & n < len e implies f . n <= f . (n + 1) )
assume that
A4: n <> 0 and
A5: n < len e ; ::_thesis: f . n <= f . (n + 1)
 ( n + 1 >= 1 & n + 1 <= len e ) by A5, NAT_1:13, NAT_1:14;
then  n + 1 in dom e by FINSEQ_3:25;
then  (f . n) + (e . (n + 1)) >= f . n by A1, XREAL_1:31;
hence  f . n <= f . (n + 1) by A2, A4, A5; ::_thesis: verum
end;
 for n being Nat st n in dom e holds
for m being Nat st m in dom e & n <= m holds
f . n <= f . m
proof
let n be Nat; ::_thesis: ( n in dom e implies for m being Nat st m in dom e & n <= m holds
f . n <= f . m )
assume  n in dom e ; ::_thesis: for m being Nat st m in dom e & n <= m holds
f . n <= f . m
then A6: n >= 1 by FINSEQ_3:25;
defpred S1[ Nat] means ( $1 in dom e & n <= $1 implies f . $1 >= f . n );
A7: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_(_k_+_1_in_dom_e_&_n_<=_k_+_1_implies_f_._(k_+_1)_>=_f_._n_)
assume that
A9: k + 1 in dom e and
A10: n <= k + 1 ; ::_thesis: f . (k + 1) >= f . n
A11: k + 1 <= len e by A9, FINSEQ_3:25;
percases ( ( k + 1 = n & k < len e ) or ( k >= n & k < len e ) ) by A10, A11, NAT_1:8, NAT_1:13;
suppose ( k + 1 = n & k < len e ) ; ::_thesis: f . (k + 1) >= f . n
hence  f . (k + 1) >= f . n ; ::_thesis: verum
end;
supposeA12: ( k >= n & k < len e ) ; ::_thesis: f . (k + 1) >= f . n
then  ( k >= 1 & f . (k + 1) >= f . k ) by A3, A6, NAT_1:14;
hence  f . (k + 1) >= f . n by A8, A12, FINSEQ_3:25, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A13: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A7);
hence  for m being Nat st m in dom e & n <= m holds
f . n <= f . m ; ::_thesis: verum
end;
hence  for n, m being Nat st n in dom e & m in dom e & n <= m holds
f . n <= f . m ; ::_thesis: verum
end;

theorem Th4: :: MATRPROB:4
for e being FinSequence of REAL st len e >= 1 & ( for i being Nat st i in dom e holds
0 <= e . i ) holds
for f being Real_Sequence st f . 1 = e . 1 & ( for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) holds
for n being Nat st n in dom e holds
e . n <= f . n
proof
let e be FinSequence of REAL ; ::_thesis: ( len e >= 1 & ( for i being Nat st i in dom e holds
0 <= e . i ) implies for f being Real_Sequence st f . 1 = e . 1 & ( for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) holds
for n being Nat st n in dom e holds
e . n <= f . n )
assume that
A1: len e >= 1 and
A2: for i being Nat st i in dom e holds
0 <= e . i ; ::_thesis: for f being Real_Sequence st f . 1 = e . 1 & ( for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) holds
for n being Nat st n in dom e holds
e . n <= f . n
let f be Real_Sequence; ::_thesis: ( f . 1 = e . 1 & ( for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) implies for n being Nat st n in dom e holds
e . n <= f . n )
assume that
A3: f . 1 = e . 1 and
A4: for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ; ::_thesis: for n being Nat st n in dom e holds
e . n <= f . n
defpred S1[ Nat] means ( $1 in dom e implies e . $1 <= f . $1 );
A5: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume  S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_(_k_+_1_in_dom_e_implies_e_._(k_+_1)_<=_f_._(k_+_1)_)
assume  k + 1 in dom e ; ::_thesis: e . (k + 1) <= f . (k + 1)
then A6: k + 1 <= len e by FINSEQ_3:25;
percases ( ( k = 0 & k < len e ) or ( k > 0 & k < len e ) ) by A6, NAT_1:13;
suppose ( k = 0 & k < len e ) ; ::_thesis: e . (k + 1) <= f . (k + 1)
hence  e . (k + 1) <= f . (k + 1) by A3; ::_thesis: verum
end;
supposeA7: ( k > 0 & k < len e ) ; ::_thesis: e . (k + 1) <= f . (k + 1)
then  1 <= len e by NAT_1:14;
then A8: 1 in dom e by FINSEQ_3:25;
A9: 1 in dom e by A1, FINSEQ_3:25;
A10: k >= 1 by A7, NAT_1:14;
then  k in dom e by A7, FINSEQ_3:25;
then  e . 1 <= f . k by A2, A3, A4, A10, A8, Th3;
then  f . k >= 0 by A2, A9;
then  (f . k) + (e . (k + 1)) >= e . (k + 1) by XREAL_1:31;
hence  e . (k + 1) <= f . (k + 1) by A4, A7; ::_thesis: verum
end;
end;
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A11: S1[ 0 ] by FINSEQ_3:25;
 for n being Nat holds S1[n] from NAT_1:sch_2(A11, A5);
hence  for n being Nat st n in dom e holds
e . n <= f . n ; ::_thesis: verum
end;

theorem Th5: :: MATRPROB:5
for e being FinSequence of REAL st ( for i being Nat st i in dom e holds
0 <= e . i ) holds
for k being Nat st k in dom e holds
e . k <= Sum e
proof
let e be FinSequence of REAL ; ::_thesis: ( ( for i being Nat st i in dom e holds
0 <= e . i ) implies for k being Nat st k in dom e holds
e . k <= Sum e )
assume A1: for i being Nat st i in dom e holds
0 <= e . i ; ::_thesis: for k being Nat st k in dom e holds
e . k <= Sum e
percases ( len e = 0 or len e <> 0 ) ;
suppose len e = 0 ; ::_thesis: for k being Nat st k in dom e holds
e . k <= Sum e
then  e = {} ;
hence  for k being Nat st k in dom e holds
e . k <= Sum e ; ::_thesis: verum
end;
supposeA2: len e <> 0 ; ::_thesis: for k being Nat st k in dom e holds
e . k <= Sum e
then  len e >= 1 by NAT_1:14;
then A3: len e in dom e by FINSEQ_3:25;
let n be Nat; ::_thesis: ( n in dom e implies e . n <= Sum e )
assume A4: n in dom e ; ::_thesis: e . n <= Sum e
reconsider n = n as Element of NAT by ORDINAL1:def_12;
consider f being Real_Sequence such that
A5: f . 1 = e . 1 and
A6: for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) and
A7: Sum e = f . (len e) by A2, NAT_1:14, PROB_3:63;
A8: e . n <= f . n by A1, A2, A5, A6, A4, Th4, NAT_1:14;
 n <= len e by A4, FINSEQ_3:25;
then  f . n <= f . (len e) by A1, A6, A4, A3, Th3;
hence  e . n <= Sum e by A7, A8, XXREAL_0:2; ::_thesis: verum
end;
end;
end;

theorem Th6: :: MATRPROB:6
for r1, r2 being Real
for k being Nat
for seq1 being Real_Sequence ex seq being Real_Sequence st
( seq . 0 = r1 & ( for n being Nat holds
( ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n > k implies seq . n = r2 ) ) ) )
proof
let r1, r2 be Real; ::_thesis: for k being Nat
for seq1 being Real_Sequence ex seq being Real_Sequence st
( seq . 0 = r1 & ( for n being Nat holds
( ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n > k implies seq . n = r2 ) ) ) )
let k be Nat; ::_thesis: for seq1 being Real_Sequence ex seq being Real_Sequence st
( seq . 0 = r1 & ( for n being Nat holds
( ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n > k implies seq . n = r2 ) ) ) )
let seq1 be Real_Sequence; ::_thesis: ex seq being Real_Sequence st
( seq . 0 = r1 & ( for n being Nat holds
( ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n > k implies seq . n = r2 ) ) ) )
 ex seq being Real_Sequence st
for n being Nat holds
( ( n = 0 implies seq . n = r1 ) & ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n <> 0 & n > k implies seq . n = r2 ) )
proof
defpred S1[ set , set ] means  ex n being Element of NAT st
( n = $1 & ( n = 0 implies $2 = r1 ) & ( n <> 0 & n <= k implies $2 = seq1 . n ) & ( n <> 0 & n > k implies $2 = r2 ) );
A1: for x being set st x in NAT holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st S1[x,y] )
assume  x in NAT ; ::_thesis: ex y being set st S1[x,y]
then reconsider n = x as Element of NAT ;
now__::_thesis:_(_(_n_=_0_&_S1[x,r1]_)_or_(_n_<>_0_&_n_<=_k_&_S1[x,seq1_._n]_)_or_(_n_<>_0_&_not_n_<=_k_&_S1[x,r2]_)_)
percases ( n = 0 or ( n <> 0 & n <= k ) or ( n <> 0 & not n <= k ) ) ;
case n = 0 ; ::_thesis: S1[x,r1]
hence  S1[x,r1] ; ::_thesis: verum
end;
case ( n <> 0 & n <= k ) ; ::_thesis: S1[x,seq1 . n]
hence  S1[x,seq1 . n] ; ::_thesis: verum
end;
case ( n <> 0 & not n <= k ) ; ::_thesis: S1[x,r2]
hence  S1[x,r2] ; ::_thesis: verum
end;
end;
end;
hence  ex y being set st S1[x,y] ; ::_thesis: verum
end;
consider f1 being Function such that
A2: ( dom f1 = NAT & ( for x being set st x in NAT holds
S1[x,f1 . x] ) ) from CLASSES1:sch_1(A1);
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
f1_._x_is_real
let x be set ; ::_thesis: ( x in NAT implies f1 . x is real )
assume  x in NAT ; ::_thesis: f1 . x is real
then  ex n being Element of NAT st
( n = x & ( n = 0 implies f1 . x = r1 ) & ( n <> 0 & n <= k implies f1 . x = seq1 . n ) & ( n <> 0 & n > k implies f1 . x = r2 ) ) by A2;
hence  f1 . x is real ; ::_thesis: verum
end;
then reconsider f1 = f1 as Real_Sequence by A2, SEQ_1:1;
take seq = f1; ::_thesis: for n being Nat holds
( ( n = 0 implies seq . n = r1 ) & ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n <> 0 & n > k implies seq . n = r2 ) )
let n be Nat; ::_thesis: ( ( n = 0 implies seq . n = r1 ) & ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n <> 0 & n > k implies seq . n = r2 ) )
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 ex k1 being Element of NAT st
( k1 = n & ( k1 = 0 implies seq . n = r1 ) & ( k1 <> 0 & k1 <= k implies seq . n = seq1 . k1 ) & ( k1 <> 0 & k1 > k implies seq . n = r2 ) ) by A2;
hence  ( ( n = 0 implies seq . n = r1 ) & ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n <> 0 & n > k implies seq . n = r2 ) ) ; ::_thesis: verum
end;
then consider seq being Real_Sequence such that
A3: for n being Nat holds
( ( n = 0 implies seq . n = r1 ) & ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n <> 0 & n > k implies seq . n = r2 ) ) ;
take  seq ; ::_thesis: ( seq . 0 = r1 & ( for n being Nat holds
( ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n > k implies seq . n = r2 ) ) ) )
thus  ( seq . 0 = r1 & ( for n being Nat holds
( ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n > k implies seq . n = r2 ) ) ) ) by A3; ::_thesis: verum
end;

theorem Th7: :: MATRPROB:7
for F being FinSequence of REAL ex f being Real_Sequence st
( f . 0 = 0 & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) & Sum F = f . (len F) )
proof
let F be FinSequence of REAL ; ::_thesis: ex f being Real_Sequence st
( f . 0 = 0 & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) & Sum F = f . (len F) )
percases ( len F = 0 or len F > 0 ) ;
supposeA1: len F = 0 ; ::_thesis: ex f being Real_Sequence st
( f . 0 = 0 & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) & Sum F = f . (len F) )
set f = NAT --> 0;
A2: for i being Nat st i < len F holds
(NAT --> 0) . (i + 1) = ((NAT --> 0) . i) + (F . (i + 1)) by A1;
A3: for i being Nat holds (NAT --> 0) . i = 0
proof
let i be Nat; ::_thesis: (NAT --> 0) . i = 0
 i in NAT by ORDINAL1:def_12;
hence  (NAT --> 0) . i = 0 by FUNCOP_1:7; ::_thesis: verum
end;
then A4: (NAT --> 0) . 0 = 0 ;
Sum F = 0 by A1, PROB_3:62
.= (NAT --> 0) . (len F) by A3 ;
hence  ex f being Real_Sequence st
( f . 0 = 0 & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) & Sum F = f . (len F) ) by A2, A4; ::_thesis: verum
end;
supposeA5: len F > 0 ; ::_thesis: ex f being Real_Sequence st
( f . 0 = 0 & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) & Sum F = f . (len F) )
then consider f being Real_Sequence such that
A6: f . 1 = F . 1 and
A7: for i being Nat st 0 <> i & i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) and
A8: Sum F = f . (len F) by NAT_1:14, PROB_3:63;
consider f1 being Real_Sequence such that
A9: for n being Nat holds
( f1 . 0 = 0 & ( n <> 0 & n <= len F implies f1 . n = f . n ) & ( n > len F implies f1 . n = 0 ) ) by Th6;
A10: len F >= 1 by A5, NAT_1:14;
A11: for i being Nat st i < len F holds
f1 . (i + 1) = (f1 . i) + (F . (i + 1))
proof
let i be Nat; ::_thesis: ( i < len F implies f1 . (i + 1) = (f1 . i) + (F . (i + 1)) )
assume A12: i < len F ; ::_thesis: f1 . (i + 1) = (f1 . i) + (F . (i + 1))
set r = F . (i + 1);
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: f1 . (i + 1) = (f1 . i) + (F . (i + 1))
hence  f1 . (i + 1) = (f1 . i) + (F . (i + 1)) by A10, A6, A9; ::_thesis: verum
end;
supposeA13: i <> 0 ; ::_thesis: f1 . (i + 1) = (f1 . i) + (F . (i + 1))
 i + 1 <= len F by A12, NAT_1:13;
hence f1 . (i + 1) = f . (i + 1) by A9
.= (f . i) + (F . (i + 1)) by A7, A12, A13
.= (f1 . i) + (F . (i + 1)) by A9, A12, A13 ;
::_thesis: verum
end;
end;
end;
 Sum F = f1 . (len F) by A5, A8, A9;
hence  ex f being Real_Sequence st
( f . 0 = 0 & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) & Sum F = f . (len F) ) by A9, A11; ::_thesis: verum
end;
end;
end;

theorem Th8: :: MATRPROB:8
for n being Nat
for D being set
for e1 being FinSequence of D holds n |-> e1 is FinSequence of D *
proof
let n be Nat; ::_thesis: for D being set
for e1 being FinSequence of D holds n |-> e1 is FinSequence of D *
let D be set ; ::_thesis: for e1 being FinSequence of D holds n |-> e1 is FinSequence of D *
let e1 be FinSequence of D; ::_thesis: n |-> e1 is FinSequence of D *
 e1 in D * by FINSEQ_1:def_11;
hence  n |-> e1 is FinSequence of D * by FINSEQ_2:63; ::_thesis: verum
end;

theorem Th9: :: MATRPROB:9
for k being Element of NAT
for n being Nat
for D being set
for e1, e2 being FinSequence of D ex e being FinSequence of D * st
( len e = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) ) ) )
proof
let k be Element of NAT ; ::_thesis: for n being Nat
for D being set
for e1, e2 being FinSequence of D ex e being FinSequence of D * st
( len e = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) ) ) )
let n be Nat; ::_thesis: for D being set
for e1, e2 being FinSequence of D ex e being FinSequence of D * st
( len e = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) ) ) )
let D be set ; ::_thesis: for e1, e2 being FinSequence of D ex e being FinSequence of D * st
( len e = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) ) ) )
let e1, e2 be FinSequence of D; ::_thesis: ex e being FinSequence of D * st
( len e = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) ) ) )
 ( e1 in D * & e2 in D * ) by FINSEQ_1:def_11;
hence  ex e being FinSequence of D * st
( len e = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) ) ) ) by Th2; ::_thesis: verum
end;

theorem Th10: :: MATRPROB:10
for D being set
for s being FinSequence holds
( s is Matrix of D iff ex n being Nat st
for i being Element of NAT st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n ) )
proof
let D be set ; ::_thesis: for s being FinSequence holds
( s is Matrix of D iff ex n being Nat st
for i being Element of NAT st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n ) )
let s be FinSequence; ::_thesis: ( s is Matrix of D iff ex n being Nat st
for i being Element of NAT st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n ) )
thus  ( s is Matrix of D implies ex n being Nat st
for i being Element of NAT st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n ) ) ::_thesis: ( ex n being Nat st
for i being Element of NAT st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n ) implies s is Matrix of D )
proof
assume A1: s is Matrix of D ; ::_thesis: ex n being Nat st
for i being Element of NAT st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n )
then reconsider v = s as FinSequence of D * ;
consider n being Nat such that
A2: for x being set st x in rng v holds
ex t being FinSequence st
( t = x & len t = n ) by A1, MATRIX_1:def_1;
A3: for i being Element of NAT st i in dom v holds
ex p being FinSequence of D st
( v . i = p & len p = n )
proof
let i be Element of NAT ; ::_thesis: ( i in dom v implies ex p being FinSequence of D st
( v . i = p & len p = n ) )
assume  i in dom v ; ::_thesis: ex p being FinSequence of D st
( v . i = p & len p = n )
then consider t being FinSequence such that
A4: ( t = v . i & len t = n ) by A2, FUNCT_1:3;
take  t ; ::_thesis: ( t is Element of bool [:NAT,D:] & t is FinSequence of D & v . i = t & len t = n )
thus  ( t is Element of bool [:NAT,D:] & t is FinSequence of D & v . i = t & len t = n ) by A4; ::_thesis: verum
end;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
take  n ; ::_thesis: for i being Element of NAT st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n )
thus  for i being Element of NAT st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n ) by A3; ::_thesis: verum
end;
given n being Nat such that A5: for i being Element of NAT st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n ) ; ::_thesis: s is Matrix of D
A6: for x being set st x in rng s holds
( ex v being FinSequence st
( v = x & len v = n ) & x in D * )
proof
let x be set ; ::_thesis: ( x in rng s implies ( ex v being FinSequence st
( v = x & len v = n ) & x in D * ) )
assume  x in rng s ; ::_thesis: ( ex v being FinSequence st
( v = x & len v = n ) & x in D * )
then consider i being set  such that
A7: i in dom s and
A8: x = s . i by FUNCT_1:def_3;
A9: ex p being FinSequence of D st
( s . i = p & len p = n ) by A5, A7;
hence  ex v being FinSequence st
( v = x & len v = n ) by A8; ::_thesis: x in D *
thus  x in D * by A8, A9, FINSEQ_1:def_11; ::_thesis: verum
end;
then  for x being set st x in rng s holds
x in D * ;
then A10: rng s c= D * by TARSKI:def_3;
 for x being set st x in rng s holds
ex v being FinSequence st
( v = x & len v = n ) by A6;
hence  s is Matrix of D by A10, FINSEQ_1:def_4, MATRIX_1:def_1; ::_thesis: verum
end;

theorem Th11: :: MATRPROB:11
for D being set
for e being FinSequence of D * holds
( ex n being Nat st
for i being Element of NAT st i in dom e holds
len (e . i) = n iff e is Matrix of D )
proof
let D be set ; ::_thesis: for e being FinSequence of D * holds
( ex n being Nat st
for i being Element of NAT st i in dom e holds
len (e . i) = n iff e is Matrix of D )
let e be FinSequence of D * ; ::_thesis: ( ex n being Nat st
for i being Element of NAT st i in dom e holds
len (e . i) = n iff e is Matrix of D )
hereby  ::_thesis: ( e is Matrix of D implies ex n being Nat st
for i being Element of NAT st i in dom e holds
len (e . i) = n )
given n being Nat such that A1: for i being Element of NAT st i in dom e holds
len (e . i) = n ; ::_thesis: e is Matrix of D
 for i being Element of NAT st i in dom e holds
ex p being FinSequence of D st
( e . i = p & len p = n )
proof
let i be Element of NAT ; ::_thesis: ( i in dom e implies ex p being FinSequence of D st
( e . i = p & len p = n ) )
assume  i in dom e ; ::_thesis: ex p being FinSequence of D st
( e . i = p & len p = n )
then  len (e . i) = n by A1;
hence  ex p being FinSequence of D st
( e . i = p & len p = n ) ; ::_thesis: verum
end;
hence  e is Matrix of D by Th10; ::_thesis: verum
end;
assume  e is Matrix of D ; ::_thesis: ex n being Nat st
for i being Element of NAT st i in dom e holds
len (e . i) = n
then consider n being Nat such that
A2: for i being Element of NAT st i in dom e holds
ex p being FinSequence of D st
( e . i = p & len p = n ) by Th10;
 for i being Element of NAT st i in dom e holds
len (e . i) = n
proof
let i be Element of NAT ; ::_thesis: ( i in dom e implies len (e . i) = n )
assume  i in dom e ; ::_thesis: len (e . i) = n
then  ex p being FinSequence of D st
( e . i = p & len p = n ) by A2;
hence  len (e . i) = n ; ::_thesis: verum
end;
hence  ex n being Nat st
for i being Element of NAT st i in dom e holds
len (e . i) = n ; ::_thesis: verum
end;

theorem Th12: :: MATRPROB:12
for i, j being Element of NAT
for M being tabular FinSequence holds
( [i,j] in Indices M iff ( i in Seg (len M) & j in Seg (width M) ) )
proof
let i, j be Element of NAT ; ::_thesis: for M being tabular FinSequence holds
( [i,j] in Indices M iff ( i in Seg (len M) & j in Seg (width M) ) )
let M be tabular FinSequence; ::_thesis: ( [i,j] in Indices M iff ( i in Seg (len M) & j in Seg (width M) ) )
hereby  ::_thesis: ( i in Seg (len M) & j in Seg (width M) implies [i,j] in Indices M )
assume  [i,j] in Indices M ; ::_thesis: ( i in Seg (len M) & j in Seg (width M) )
then A1: [i,j] in [:(dom M),(Seg (width M)):] by MATRIX_1:def_4;
then  i in dom M by ZFMISC_1:87;
hence  ( i in Seg (len M) & j in Seg (width M) ) by A1, FINSEQ_1:def_3, ZFMISC_1:87; ::_thesis: verum
end;
assume that
A2: i in Seg (len M) and
A3: j in Seg (width M) ; ::_thesis: [i,j] in Indices M
 i in dom M by A2, FINSEQ_1:def_3;
then  [i,j] in [:(dom M),(Seg (width M)):] by A3, ZFMISC_1:87;
hence  [i,j] in Indices M by MATRIX_1:def_4; ::_thesis: verum
end;

theorem Th13: :: MATRPROB:13
for i, j being Element of NAT
for D being non empty set
for M being Matrix of D holds
( [i,j] in Indices M iff ( i in dom M & j in dom (M . i) ) )
proof
let i, j be Element of NAT ; ::_thesis: for D being non empty set
for M being Matrix of D holds
( [i,j] in Indices M iff ( i in dom M & j in dom (M . i) ) )
let D be non empty set ; ::_thesis: for M being Matrix of D holds
( [i,j] in Indices M iff ( i in dom M & j in dom (M . i) ) )
let M be Matrix of D; ::_thesis: ( [i,j] in Indices M iff ( i in dom M & j in dom (M . i) ) )
hereby  ::_thesis: ( i in dom M & j in dom (M . i) implies [i,j] in Indices M )
assume A1: [i,j] in Indices M ; ::_thesis: ( i in dom M & j in dom (M . i) )
then A2: j in Seg (width M) by Th12;
A3: i in Seg (len M) by A1, Th12;
then  i in dom M by FINSEQ_1:def_3;
then  j in Seg (len (M . i)) by A2, MATRIX_1:42;
hence  ( i in dom M & j in dom (M . i) ) by A3, FINSEQ_1:def_3; ::_thesis: verum
end;
assume  ( i in dom M & j in dom (M . i) ) ; ::_thesis: [i,j] in Indices M
hence  [i,j] in Indices M by MATRIX_1:43; ::_thesis: verum
end;

theorem Th14: :: MATRPROB:14
for i, j being Element of NAT
for D being non empty set
for M being Matrix of D st [i,j] in Indices M holds
M * (i,j) = (M . i) . j
proof
let i, j be Element of NAT ; ::_thesis: for D being non empty set
for M being Matrix of D st [i,j] in Indices M holds
M * (i,j) = (M . i) . j
let D be non empty set ; ::_thesis: for M being Matrix of D st [i,j] in Indices M holds
M * (i,j) = (M . i) . j
let M be Matrix of D; ::_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  ex p being FinSequence of D st
( p = M . i & M * (i,j) = p . j ) by MATRIX_1:def_5;
hence  M * (i,j) = (M . i) . j ; ::_thesis: verum
end;

theorem Th15: :: MATRPROB:15
for i, j being Element of NAT
for D being non empty set
for M being Matrix of D holds
( [i,j] in Indices M iff ( i in dom (Col (M,j)) & j in dom (Line (M,i)) ) )
proof
let i, j be Element of NAT ; ::_thesis: for D being non empty set
for M being Matrix of D holds
( [i,j] in Indices M iff ( i in dom (Col (M,j)) & j in dom (Line (M,i)) ) )
let D be non empty set ; ::_thesis: for M being Matrix of D holds
( [i,j] in Indices M iff ( i in dom (Col (M,j)) & j in dom (Line (M,i)) ) )
let M be Matrix of D; ::_thesis: ( [i,j] in Indices M iff ( i in dom (Col (M,j)) & j in dom (Line (M,i)) ) )
hereby  ::_thesis: ( i in dom (Col (M,j)) & j in dom (Line (M,i)) implies [i,j] in Indices M )
assume A1: [i,j] in Indices M ; ::_thesis: ( i in dom (Col (M,j)) & j in dom (Line (M,i)) )
then A2: i in dom M by Th13;
then  i in Seg (len M) by FINSEQ_1:def_3;
then  i in Seg (len (Col (M,j))) by MATRIX_1:def_8;
hence  i in dom (Col (M,j)) by FINSEQ_1:def_3; ::_thesis: j in dom (Line (M,i))
 j in dom (M . i) by A1, Th13;
hence  j in dom (Line (M,i)) by A2, MATRIX_2:16; ::_thesis: verum
end;
assume that
A3: i in dom (Col (M,j)) and
A4: j in dom (Line (M,i)) ; ::_thesis: [i,j] in Indices M
 i in Seg (len (Col (M,j))) by A3, FINSEQ_1:def_3;
then  i in Seg (len M) by MATRIX_1:def_8;
then A5: i in dom M by FINSEQ_1:def_3;
then  j in dom (M . i) by A4, MATRIX_2:16;
hence  [i,j] in Indices M by A5, Th13; ::_thesis: verum
end;

theorem Th16: :: MATRPROB:16
for D1, D2 being non empty set
for M1 being Matrix of D1
for M2 being Matrix of D2 st M1 = M2 holds
for i being Element of NAT st i in dom M1 holds
Line (M1,i) = Line (M2,i)
proof
let D1, D2 be non empty set ; ::_thesis: for M1 being Matrix of D1
for M2 being Matrix of D2 st M1 = M2 holds
for i being Element of NAT st i in dom M1 holds
Line (M1,i) = Line (M2,i)
let M1 be Matrix of D1; ::_thesis: for M2 being Matrix of D2 st M1 = M2 holds
for i being Element of NAT st i in dom M1 holds
Line (M1,i) = Line (M2,i)
let M2 be Matrix of D2; ::_thesis: ( M1 = M2 implies for i being Element of NAT st i in dom M1 holds
Line (M1,i) = Line (M2,i) )
assume A1: M1 = M2 ; ::_thesis: for i being Element of NAT st i in dom M1 holds
Line (M1,i) = Line (M2,i)
hereby  ::_thesis: verum
let i be Element of NAT ; ::_thesis: ( i in dom M1 implies Line (M1,i) = Line (M2,i) )
assume A2: i in dom M1 ; ::_thesis: Line (M1,i) = Line (M2,i)
then  Line (M1,i) = M1 . i by MATRIX_2:16;
hence  Line (M1,i) = Line (M2,i) by A1, A2, MATRIX_2:16; ::_thesis: verum
end;
end;

theorem Th17: :: MATRPROB:17
for D1, D2 being non empty set
for M1 being Matrix of D1
for M2 being Matrix of D2 st M1 = M2 holds
for j being Element of NAT st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j)
proof
let D1, D2 be non empty set ; ::_thesis: for M1 being Matrix of D1
for M2 being Matrix of D2 st M1 = M2 holds
for j being Element of NAT st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j)
let M1 be Matrix of D1; ::_thesis: for M2 being Matrix of D2 st M1 = M2 holds
for j being Element of NAT st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j)
let M2 be Matrix of D2; ::_thesis: ( M1 = M2 implies for j being Element of NAT st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j) )
assume A1: M1 = M2 ; ::_thesis: for j being Element of NAT st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j)
hereby  ::_thesis: verum
let j be Element of NAT ; ::_thesis: ( j in Seg (width M1) implies Col (M1,j) = Col (M2,j) )
assume A2: j in Seg (width M1) ; ::_thesis: Col (M1,j) = Col (M2,j)
A3: for k being Nat st k in dom (Col (M1,j)) holds
(Col (M1,j)) . k = (Col (M2,j)) . k
proof
let k be Nat; ::_thesis: ( k in dom (Col (M1,j)) implies (Col (M1,j)) . k = (Col (M2,j)) . k )
assume  k in dom (Col (M1,j)) ; ::_thesis: (Col (M1,j)) . k = (Col (M2,j)) . k
then  k in Seg (len (Col (M1,j))) by FINSEQ_1:def_3;
then A4: k in Seg (len M1) by MATRIX_1:def_8;
then A5: [k,j] in Indices M1 by A2, Th12;
A6: k in dom M1 by A4, FINSEQ_1:def_3;
hence (Col (M1,j)) . k = M1 * (k,j) by MATRIX_1:def_8
.= M2 * (k,j) by A1, A5, MATRIXR1:23
.= (Col (M2,j)) . k by A1, A6, MATRIX_1:def_8 ;
::_thesis: verum
end;
dom (Col (M1,j)) = Seg (len (Col (M1,j))) by FINSEQ_1:def_3
.= Seg (len M1) by MATRIX_1:def_8
.= Seg (len (Col (M2,j))) by A1, MATRIX_1:def_8
.= dom (Col (M2,j)) by FINSEQ_1:def_3 ;
hence  Col (M1,j) = Col (M2,j) by A3, FINSEQ_1:13; ::_thesis: verum
end;
end;

theorem Th18: :: MATRPROB:18
for D being non empty set
for m, n being Nat
for e1 being FinSequence of D st len e1 = m holds
n |-> e1 is Matrix of n,m,D
proof
let D be non empty set ; ::_thesis: for m, n being Nat
for e1 being FinSequence of D st len e1 = m holds
n |-> e1 is Matrix of n,m,D
let m, n be Nat; ::_thesis: for e1 being FinSequence of D st len e1 = m holds
n |-> e1 is Matrix of n,m,D
let e1 be FinSequence of D; ::_thesis: ( len e1 = m implies n |-> e1 is Matrix of n,m,D )
assume A1: len e1 = m ; ::_thesis: n |-> e1 is Matrix of n,m,D
reconsider e = n |-> e1 as FinSequence of D * by Th8;
A2: len e = n by CARD_1:def_7;
A3: for i being Element of NAT st i in dom e holds
len (e . i) = m
proof
let i be Element of NAT ; ::_thesis: ( i in dom e implies len (e . i) = m )
assume  i in dom e ; ::_thesis: len (e . i) = m
then  i in Seg n by A2, FINSEQ_1:def_3;
hence  len (e . i) = m by A1, FUNCOP_1:7; ::_thesis: verum
end;
then reconsider e = e as Matrix of D by Th11;
 for p being FinSequence of D st p in rng e holds
len p = m
proof
let p be FinSequence of D; ::_thesis: ( p in rng e implies len p = m )
assume  p in rng e ; ::_thesis: len p = m
then  ex i being set st
( i in dom e & p = e . i ) by FUNCT_1:def_3;
hence  len p = m by A3; ::_thesis: verum
end;
hence  n |-> e1 is Matrix of n,m,D by A2, MATRIX_1:def_2; ::_thesis: verum
end;

theorem Th19: :: MATRPROB:19
for D being non empty set
for k being Element of NAT
for m, n being Nat
for e1, e2 being FinSequence of D st len e1 = m & len e2 = m holds
ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) )
proof
let D be non empty set ; ::_thesis: for k being Element of NAT
for m, n being Nat
for e1, e2 being FinSequence of D st len e1 = m & len e2 = m holds
ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) )
let k be Element of NAT ; ::_thesis: for m, n being Nat
for e1, e2 being FinSequence of D st len e1 = m & len e2 = m holds
ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) )
let m, n be Nat; ::_thesis: for e1, e2 being FinSequence of D st len e1 = m & len e2 = m holds
ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) )
let e1, e2 be FinSequence of D; ::_thesis: ( len e1 = m & len e2 = m implies ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) ) )
assume A1: ( len e1 = m & len e2 = m ) ; ::_thesis: ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) )
consider e being FinSequence of D *  such that
A2: len e = n and
A3: for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) ) by Th9;
A4: for i being Element of NAT st i in dom e holds
len (e . i) = m
proof
let i be Element of NAT ; ::_thesis: ( i in dom e implies len (e . i) = m )
assume  i in dom e ; ::_thesis: len (e . i) = m
then  i in Seg n by A2, FINSEQ_1:def_3;
hence  len (e . i) = m by A1, A3; ::_thesis: verum
end;
then reconsider e = e as Matrix of D by Th11;
 for p being FinSequence of D st p in rng e holds
len p = m
proof
let p be FinSequence of D; ::_thesis: ( p in rng e implies len p = m )
assume  p in rng e ; ::_thesis: len p = m
then  ex i being set st
( i in dom e & p = e . i ) by FUNCT_1:def_3;
hence  len p = m by A4; ::_thesis: verum
end;
then  e is Matrix of n,m,D by A2, MATRIX_1:def_2;
hence  ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) ) by A3; ::_thesis: verum
end;

Lm1:  for r being Real
for m being Matrix of REAL holds
( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of NAT st i in dom m & j in dom (m . i) holds
(m . i) . j >= r )
proof
let r be Real; ::_thesis: for m being Matrix of REAL holds
( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of NAT st i in dom m & j in dom (m . i) holds
(m . i) . j >= r )
let m be Matrix of REAL; ::_thesis: ( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of NAT st i in dom m & j in dom (m . i) holds
(m . i) . j >= r )
hereby  ::_thesis: ( ( for i, j being Element of NAT st i in dom m & j in dom (m . i) holds
(m . i) . j >= r ) implies for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r )
assume A1: for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ; ::_thesis: for i, j being Element of NAT st i in dom m & j in dom (m . i) holds
(m . i) . j >= r
hereby  ::_thesis: verum
let i, j be Element of NAT ; ::_thesis: ( i in dom m & j in dom (m . i) implies (m . i) . j >= r )
assume  ( i in dom m & j in dom (m . i) ) ; ::_thesis: (m . i) . j >= r
then A2: [i,j] in Indices m by Th13;
then  m * (i,j) >= r by A1;
hence  (m . i) . j >= r by A2, Th14; ::_thesis: verum
end;
end;
assume A3: for i, j being Element of NAT st i in dom m & j in dom (m . i) holds
(m . i) . j >= r ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r
hereby  ::_thesis: verum
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices m implies m * (i,j) >= r )
assume A4: [i,j] in Indices m ; ::_thesis: m * (i,j) >= r
 ( i in dom m & j in dom (m . i) ) by A4, Th13;
then  (m . i) . j >= r by A3;
hence  m * (i,j) >= r by A4, Th14; ::_thesis: verum
end;
end;

Lm2:  for r being Real
for m being Matrix of REAL holds
( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of NAT st i in dom m & j in dom (Line (m,i)) holds
(Line (m,i)) . j >= r )
proof
let r be Real; ::_thesis: for m being Matrix of REAL holds
( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of NAT st i in dom m & j in dom (Line (m,i)) holds
(Line (m,i)) . j >= r )
let m be Matrix of REAL; ::_thesis: ( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of NAT st i in dom m & j in dom (Line (m,i)) holds
(Line (m,i)) . j >= r )
hereby  ::_thesis: ( ( for i, j being Element of NAT st i in dom m & j in dom (Line (m,i)) holds
(Line (m,i)) . j >= r ) implies for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r )
assume A1: for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ; ::_thesis: for i, j being Element of NAT st i in dom m & j in dom (Line (m,i)) holds
(Line (m,i)) . j >= r
hereby  ::_thesis: verum
let i, j be Element of NAT ; ::_thesis: ( i in dom m & j in dom (Line (m,i)) implies (Line (m,i)) . j >= r )
assume that
A2: i in dom m and
A3: j in dom (Line (m,i)) ; ::_thesis: (Line (m,i)) . j >= r
 m . i = Line (m,i) by A2, MATRIX_2:16;
hence  (Line (m,i)) . j >= r by A1, A2, A3, Lm1; ::_thesis: verum
end;
end;
assume A4: for i, j being Element of NAT st i in dom m & j in dom (Line (m,i)) holds
(Line (m,i)) . j >= r ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_m_holds_
for_j_being_Element_of_NAT_st_j_in_dom_(m_._i)_holds_
(m_._i)_._j_>=_r
let i be Element of NAT ; ::_thesis: ( i in dom m implies for j being Element of NAT st j in dom (m . i) holds
(m . i) . j >= r )
assume A5: i in dom m ; ::_thesis: for j being Element of NAT st j in dom (m . i) holds
(m . i) . j >= r
 m . i = Line (m,i) by A5, MATRIX_2:16;
hence  for j being Element of NAT st j in dom (m . i) holds
(m . i) . j >= r by A4, A5; ::_thesis: verum
end;
then  for i, j being Element of NAT st i in dom m & j in dom (m . i) holds
(m . i) . j >= r ;
hence  for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r by Lm1; ::_thesis: verum
end;

Lm3:  for r being Real
for m being Matrix of REAL holds
( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of NAT st j in Seg (width m) & i in dom (Col (m,j)) holds
(Col (m,j)) . i >= r )
proof
let r be Real; ::_thesis: for m being Matrix of REAL holds
( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of NAT st j in Seg (width m) & i in dom (Col (m,j)) holds
(Col (m,j)) . i >= r )
let m be Matrix of REAL; ::_thesis: ( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Element of NAT st j in Seg (width m) & i in dom (Col (m,j)) holds
(Col (m,j)) . i >= r )
hereby  ::_thesis: ( ( for i, j being Element of NAT st j in Seg (width m) & i in dom (Col (m,j)) holds
(Col (m,j)) . i >= r ) implies for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r )
assume A1: for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r ; ::_thesis: for i, j being Element of NAT st j in Seg (width m) & i in dom (Col (m,j)) holds
(Col (m,j)) . i >= r
hereby  ::_thesis: verum
let i, j be Element of NAT ; ::_thesis: ( j in Seg (width m) & i in dom (Col (m,j)) implies (Col (m,j)) . i >= r )
assume that
A2: j in Seg (width m) and
A3: i in dom (Col (m,j)) ; ::_thesis: (Col (m,j)) . i >= r
 j in Seg (len (Line (m,i))) by A2, MATRIX_1:def_7;
then A4: j in dom (Line (m,i)) by FINSEQ_1:def_3;
then  [i,j] in Indices m by A3, Th15;
then A5: i in dom m by Th13;
then  (Line (m,i)) . j >= r by A1, A4, Lm2;
hence  (Col (m,j)) . i >= r by A2, A5, GOBOARD1:2; ::_thesis: verum
end;
end;
assume A6: for i, j being Element of NAT st j in Seg (width m) & i in dom (Col (m,j)) holds
(Col (m,j)) . i >= r ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r
 for i, j being Element of NAT st i in dom m & j in dom (Line (m,i)) holds
(Line (m,i)) . j >= r
proof
let i, j be Element of NAT ; ::_thesis: ( i in dom m & j in dom (Line (m,i)) implies (Line (m,i)) . j >= r )
assume that
A7: i in dom m and
A8: j in dom (Line (m,i)) ; ::_thesis: (Line (m,i)) . j >= r
 j in Seg (len (Line (m,i))) by A8, FINSEQ_1:def_3;
then A9: j in Seg (width m) by MATRIX_1:def_7;
 i in Seg (len m) by A7, FINSEQ_1:def_3;
then  i in Seg (len (Col (m,j))) by MATRIX_1:def_8;
then  i in dom (Col (m,j)) by FINSEQ_1:def_3;
then  (Col (m,j)) . i >= r by A6, A9;
hence  (Line (m,i)) . j >= r by A7, A9, GOBOARD1:2; ::_thesis: verum
end;
hence  for i, j being Element of NAT st [i,j] in Indices m holds
m * (i,j) >= r by Lm2; ::_thesis: verum
end;

definition
let e be FinSequence of REAL * ;
func Sum e ->  FinSequence of REAL  means :Def1: :: MATRPROB:def 1
( len it = len e & ( for k being Element of NAT st k in dom it holds
it . k = Sum (e . k) ) );
existence
 ex b1 being FinSequence of REAL st
( len b1 = len e & ( for k being Element of NAT st k in dom b1 holds
b1 . k = Sum (e . k) ) )
proof
deffunc H1( Nat) ->  Element of REAL = Sum (e . $1);
consider e1 being FinSequence of REAL  such that
A1: ( len e1 = len e & ( for k being Nat st k in dom e1 holds
e1 . k = H1(k) ) ) from FINSEQ_2:sch_1();
take  e1 ; ::_thesis: ( len e1 = len e & ( for k being Element of NAT st k in dom e1 holds
e1 . k = Sum (e . k) ) )
thus  ( len e1 = len e & ( for k being Element of NAT st k in dom e1 holds
e1 . k = Sum (e . k) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of REAL st len b1 = len e & ( for k being Element of NAT st k in dom b1 holds
b1 . k = Sum (e . k) ) & len b2 = len e & ( for k being Element of NAT st k in dom b2 holds
b2 . k = Sum (e . k) ) holds
b1 = b2
proof
let e1, e2 be FinSequence of REAL ; ::_thesis: ( len e1 = len e & ( for k being Element of NAT st k in dom e1 holds
e1 . k = Sum (e . k) ) & len e2 = len e & ( for k being Element of NAT st k in dom e2 holds
e2 . k = Sum (e . k) ) implies e1 = e2 )
assume that
A2: len e1 = len e and
A3: for k being Element of NAT st k in dom e1 holds
e1 . k = Sum (e . k) and
A4: len e2 = len e and
A5: for k being Element of NAT st k in dom e2 holds
e2 . k = Sum (e . k) ; ::_thesis: e1 = e2
 ( dom e1 = dom e2 & ( for k being Nat st k in dom e1 holds
e1 . k = e2 . k ) )
proof
thus A6: dom e1 = Seg (len e) by A2, FINSEQ_1:def_3
.= dom e2 by A4, FINSEQ_1:def_3 ; ::_thesis: for k being Nat st k in dom e1 holds
e1 . k = e2 . k
let k be Nat; ::_thesis: ( k in dom e1 implies e1 . k = e2 . k )
assume A7: k in dom e1 ; ::_thesis: e1 . k = e2 . k
thus e1 . k = Sum (e . k) by A3, A7
.= e2 . k by A5, A6, A7 ; ::_thesis: verum
end;
hence  e1 = e2 by FINSEQ_1:13; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Sum MATRPROB:def_1_:_
 for e being FinSequence of REAL *
for b2 being FinSequence of REAL holds
( b2 = Sum e iff ( len b2 = len e & ( for k being Element of NAT st k in dom b2 holds
b2 . k = Sum (e . k) ) ) );

notation
let m be Matrix of REAL;
synonym  LineSum m for  Sum m;
end;

theorem Th20: :: MATRPROB:20
for m being Matrix of REAL holds
( len (Sum m) = len m & ( for i being Element of NAT st i in Seg (len m) holds
(Sum m) . i = Sum (Line (m,i)) ) )
proof
let m be Matrix of REAL; ::_thesis: ( len (Sum m) = len m & ( for i being Element of NAT st i in Seg (len m) holds
(Sum m) . i = Sum (Line (m,i)) ) )
thus  len (Sum m) = len m by Def1; ::_thesis: for i being Element of NAT st i in Seg (len m) holds
(Sum m) . i = Sum (Line (m,i))
thus  for k being Element of NAT st k in Seg (len m) holds
(Sum m) . k = Sum (Line (m,k)) ::_thesis: verum
proof
let k be Element of NAT ; ::_thesis: ( k in Seg (len m) implies (Sum m) . k = Sum (Line (m,k)) )
assume A1: k in Seg (len m) ; ::_thesis: (Sum m) . k = Sum (Line (m,k))
A2: k in dom m by A1, FINSEQ_1:def_3;
 k in Seg (len (Sum m)) by A1, Def1;
then  k in dom (Sum m) by FINSEQ_1:def_3;
hence (Sum m) . k = Sum (m . k) by Def1
.= Sum (Line (m,k)) by A2, MATRIX_2:16 ;
::_thesis: verum
end;
end;

definition
let m be Matrix of REAL;
func ColSum m ->  FinSequence of REAL  means :Def2: :: MATRPROB:def 2
( len it = width m & ( for j being Nat st j in Seg (width m) holds
it . j = Sum (Col (m,j)) ) );
existence
 ex b1 being FinSequence of REAL st
( len b1 = width m & ( for j being Nat st j in Seg (width m) holds
b1 . j = Sum (Col (m,j)) ) )
proof
deffunc H1( Nat) ->  Element of REAL = Sum (Col (m,$1));
consider e being FinSequence of REAL  such that
A1: ( len e = width m & ( for k being Nat st k in dom e holds
e . k = H1(k) ) ) from FINSEQ_2:sch_1();
 dom e = Seg (width m) by A1, FINSEQ_1:def_3;
hence  ex b1 being FinSequence of REAL st
( len b1 = width m & ( for j being Nat st j in Seg (width m) holds
b1 . j = Sum (Col (m,j)) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of REAL st len b1 = width m & ( for j being Nat st j in Seg (width m) holds
b1 . j = Sum (Col (m,j)) ) & len b2 = width m & ( for j being Nat st j in Seg (width m) holds
b2 . j = Sum (Col (m,j)) ) holds
b1 = b2
proof
let p1, p2 be FinSequence of REAL ; ::_thesis: ( len p1 = width m & ( for j being Nat st j in Seg (width m) holds
p1 . j = Sum (Col (m,j)) ) & len p2 = width m & ( for j being Nat st j in Seg (width m) holds
p2 . j = Sum (Col (m,j)) ) implies p1 = p2 )
assume that
A2: len p1 = width m and
A3: for i being Nat st i in Seg (width m) holds
p1 . i = Sum (Col (m,i)) and
A4: len p2 = width m and
A5: for i being Nat st i in Seg (width m) holds
p2 . i = Sum (Col (m,i)) ; ::_thesis: p1 = p2
A6: dom p1 = Seg (width m) by A2, FINSEQ_1:def_3;
 for j being Nat st j in dom p1 holds
p1 . j = p2 . j
proof
let j be Nat; ::_thesis: ( j in dom p1 implies p1 . j = p2 . j )
assume A7: j in dom p1 ; ::_thesis: p1 . j = p2 . j
then  p1 . j = Sum (Col (m,j)) by A3, A6;
hence  p1 . j = p2 . j by A5, A6, A7; ::_thesis: verum
end;
hence  p1 = p2 by A2, A4, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines ColSum MATRPROB:def_2_:_
 for m being Matrix of REAL
for b2 being FinSequence of REAL holds
( b2 = ColSum m iff ( len b2 = width m & ( for j being Nat st j in Seg (width m) holds
b2 . j = Sum (Col (m,j)) ) ) );

theorem :: MATRPROB:21
for M being Matrix of REAL st width M > 0 holds
LineSum M = ColSum (M @)
proof
let M be Matrix of REAL; ::_thesis: ( width M > 0 implies LineSum M = ColSum (M @) )
assume  width M > 0 ; ::_thesis: LineSum M = ColSum (M @)
then A1: len M = width (M @) by MATRIX_2:10;
A2: len (LineSum M) = len M by Th20;
A3: len (ColSum (M @)) = width (M @) by Def2;
A4: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(ColSum_(M_@))_holds_
(ColSum_(M_@))_._i_=_(LineSum_M)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len (ColSum (M @)) implies (ColSum (M @)) . i = (LineSum M) . i )
assume that
A5: 1 <= i and
A6: i <= len (ColSum (M @)) ; ::_thesis: (ColSum (M @)) . i = (LineSum M) . i
 i <= len (LineSum M) by A2, A1, A6, Def2;
then  i in Seg (len (LineSum M)) by A5, FINSEQ_1:1;
then A7: i in Seg (len M) by Th20;
then A8: i in dom M by FINSEQ_1:def_3;
 i in Seg (width (M @)) by A3, A5, A6, FINSEQ_1:1;
hence (ColSum (M @)) . i = Sum (Col ((M @),i)) by Def2
.= Sum (Line (M,i)) by A8, MATRIX_2:14
.= (LineSum M) . i by A7, Th20 ;
::_thesis: verum
end;
 len (ColSum (M @)) = len (LineSum M) by A2, A1, Def2;
hence  LineSum M = ColSum (M @) by A4, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th22: :: MATRPROB:22
for M being Matrix of REAL holds ColSum M = LineSum (M @)
proof
let M be Matrix of REAL; ::_thesis: ColSum M = LineSum (M @)
A1: len (ColSum M) = width M by Def2;
A2: len (LineSum (M @)) = len (M @) by Th20;
A3: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(ColSum_M)_holds_
(ColSum_M)_._i_=_(LineSum_(M_@))_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len (ColSum M) implies (ColSum M) . i = (LineSum (M @)) . i )
assume that
A4: 1 <= i and
A5: i <= len (ColSum M) ; ::_thesis: (ColSum M) . i = (LineSum (M @)) . i
 i <= len (LineSum (M @)) by A2, A1, A5, MATRIX_1:def_6;
then  i in Seg (len (LineSum (M @))) by A4, FINSEQ_1:1;
then A6: i in Seg (len (M @)) by Th20;
A7: i in Seg (width M) by A1, A4, A5, FINSEQ_1:1;
hence (ColSum M) . i = Sum (Col (M,i)) by Def2
.= Sum (Line ((M @),i)) by A7, MATRIX_2:15
.= (LineSum (M @)) . i by A6, Th20 ;
::_thesis: verum
end;
 len (ColSum M) = len (LineSum (M @)) by A2, A1, MATRIX_1:def_6;
hence  ColSum M = LineSum (M @) by A3, FINSEQ_1:14; ::_thesis: verum
end;

definition
let M be Matrix of REAL;
func SumAll M ->  Element of REAL  equals :: MATRPROB:def 3
 Sum (Sum M);
coherence
 Sum (Sum M) is Element of REAL ;
end;

:: deftheorem  defines SumAll MATRPROB:def_3_:_
 for M being Matrix of REAL holds SumAll M = Sum (Sum M);

theorem Th23: :: MATRPROB:23
for M being Matrix of REAL st len M = 0 holds
SumAll M = 0
proof
let M be Matrix of REAL; ::_thesis: ( len M = 0 implies SumAll M = 0 )
assume  len M = 0 ; ::_thesis: SumAll M = 0
then  len (Sum M) = 0 by Def1;
then  Sum M = <*> REAL ;
hence  SumAll M = 0 by RVSUM_1:72; ::_thesis: verum
end;

theorem Th24: :: MATRPROB:24
for m being Nat
for M being Matrix of m, 0 , REAL holds SumAll M = 0
proof
let m be Nat; ::_thesis: for M being Matrix of m, 0 , REAL holds SumAll M = 0
let M be Matrix of m, 0 , REAL ; ::_thesis: SumAll M = 0
percases ( m = 0 or m > 0 ) ;
suppose m = 0 ; ::_thesis: SumAll M = 0
then  len M = 0 by MATRIX_1:def_2;
hence  SumAll M = 0 by Th23; ::_thesis: verum
end;
supposeA1: m > 0 ; ::_thesis: SumAll M = 0
 ( len (Sum M) > 0 & ( for k being Nat st k in dom (Sum M) holds
(Sum M) . k = 0 ) )
proof
 len M > 0 by A1, MATRIX_1:def_2;
hence  len (Sum M) > 0 by Def1; ::_thesis: for k being Nat st k in dom (Sum M) holds
(Sum M) . k = 0
 len M = len (Sum M) by Def1;
then A2: dom M = dom (Sum M) by FINSEQ_3:29;
hereby  ::_thesis: verum
let k be Nat; ::_thesis: ( k in dom (Sum M) implies (Sum M) . k = 0 )
assume A3: k in dom (Sum M) ; ::_thesis: (Sum M) . k = 0
 M . k in rng M by A2, A3, FUNCT_1:def_3;
then  len (M . k) = 0 by MATRIX_1:def_2;
then A4: M . k = <*> REAL ;
thus (Sum M) . k = Sum (M . k) by A3, Def1
.= 0 by A4, RVSUM_1:72 ; ::_thesis: verum
end;
end;
hence  SumAll M = Sum ((len (Sum M)) |-> 0) by Th1
.= (len (Sum M)) * 0 by RVSUM_1:80
.= 0 ;
::_thesis: verum
end;
end;
end;

theorem Th25: :: MATRPROB:25
for k being Element of NAT
for n, m being Nat
for M1 being Matrix of n,k, REAL
for M2 being Matrix of m,k, REAL holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
proof
let k be Element of NAT ; ::_thesis: for n, m being Nat
for M1 being Matrix of n,k, REAL
for M2 being Matrix of m,k, REAL holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
let n, m be Nat; ::_thesis: for M1 being Matrix of n,k, REAL
for M2 being Matrix of m,k, REAL holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
let M1 be Matrix of n,k, REAL ; ::_thesis: for M2 being Matrix of m,k, REAL holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
let M2 be Matrix of m,k, REAL ; ::_thesis: Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
A1: dom (Sum (M1 ^ M2)) = Seg (len (Sum (M1 ^ M2))) by FINSEQ_1:def_3;
A2: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(Sum_(M1_^_M2))_holds_
(Sum_(M1_^_M2))_._i_=_((Sum_M1)_^_(Sum_M2))_._i
let i be Nat; ::_thesis: ( i in dom (Sum (M1 ^ M2)) implies (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i )
assume A3: i in dom (Sum (M1 ^ M2)) ; ::_thesis: (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i
then  i in Seg (len (M1 ^ M2)) by A1, Def1;
then A4: i in dom (M1 ^ M2) by FINSEQ_1:def_3;
now__::_thesis:_(Sum_(M1_^_M2))_._i_=_((Sum_M1)_^_(Sum_M2))_._i
percases ( i in dom M1 or ex n being Nat st
( n in dom M2 & i = (len M1) + n ) ) by A4, FINSEQ_1:25;
supposeA5: i in dom M1 ; ::_thesis: (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i
 len M1 = len (Sum M1) by Def1;
then A6: dom M1 = dom (Sum M1) by FINSEQ_3:29;
thus (Sum (M1 ^ M2)) . i = Sum ((M1 ^ M2) . i) by A3, Def1
.= Sum (M1 . i) by A5, FINSEQ_1:def_7
.= (Sum M1) . i by A5, A6, Def1
.= ((Sum M1) ^ (Sum M2)) . i by A5, A6, FINSEQ_1:def_7 ; ::_thesis: verum
end;
supposeA7: ex n being Nat st
( n in dom M2 & i = (len M1) + n ) ; ::_thesis: (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i
A8: len M1 = len (Sum M1) by Def1;
 len M2 = len (Sum M2) by Def1;
then A9: dom M2 = dom (Sum M2) by FINSEQ_3:29;
consider n being Nat such that
A10: n in dom M2 and
A11: i = (len M1) + n by A7;
thus (Sum (M1 ^ M2)) . i = Sum ((M1 ^ M2) . i) by A3, Def1
.= Sum (M2 . n) by A10, A11, FINSEQ_1:def_7
.= (Sum M2) . n by A10, A9, Def1
.= ((Sum M1) ^ (Sum M2)) . i by A10, A11, A8, A9, FINSEQ_1:def_7 ; ::_thesis: verum
end;
end;
end;
hence  (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i ; ::_thesis: verum
end;
len (Sum (M1 ^ M2)) = len (M1 ^ M2) by Def1
.= (len M1) + (len M2) by FINSEQ_1:22
.= (len (Sum M1)) + (len M2) by Def1
.= (len (Sum M1)) + (len (Sum M2)) by Def1
.= len ((Sum M1) ^ (Sum M2)) by FINSEQ_1:22 ;
hence  Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2) by A2, FINSEQ_2:9; ::_thesis: verum
end;

theorem Th26: :: MATRPROB:26
for M1, M2 being Matrix of REAL holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)
proof
let M1, M2 be Matrix of REAL; ::_thesis: (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)
reconsider M = min ((len M1),(len M2)) as Element of NAT by FINSEQ_2:1;
A1: Seg M = (Seg (len M1)) /\ (Seg (len M2)) by FINSEQ_2:2
.= (Seg (len M1)) /\ (dom M2) by FINSEQ_1:def_3
.= (dom M1) /\ (dom M2) by FINSEQ_1:def_3
.= dom (M1 ^^ M2) by PRE_POLY:def_4
.= Seg (len (M1 ^^ M2)) by FINSEQ_1:def_3 ;
A2: len ((Sum M1) + (Sum M2)) = len (addreal .: ((Sum M1),(Sum M2)))
.= min ((len (Sum M1)),(len (Sum M2))) by FINSEQ_2:71
.= min ((len M1),(len (Sum M2))) by Def1
.= min ((len M1),(len M2)) by Def1
.= len (M1 ^^ M2) by A1, FINSEQ_1:6
.= len (Sum (M1 ^^ M2)) by Def1 ;
A3: dom ((Sum M1) + (Sum M2)) = Seg (len ((Sum M1) + (Sum M2))) by FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_((Sum_M1)_+_(Sum_M2))_holds_
((Sum_M1)_+_(Sum_M2))_._i_=_(Sum_(M1_^^_M2))_._i
let i be Nat; ::_thesis: ( i in dom ((Sum M1) + (Sum M2)) implies ((Sum M1) + (Sum M2)) . i = (Sum (M1 ^^ M2)) . i )
assume A4: i in dom ((Sum M1) + (Sum M2)) ; ::_thesis: ((Sum M1) + (Sum M2)) . i = (Sum (M1 ^^ M2)) . i
then A5: i in dom (addreal .: ((Sum M1),(Sum M2))) ;
 i in Seg (len (M1 ^^ M2)) by A2, A3, A4, Def1;
then A6: i in dom (M1 ^^ M2) by FINSEQ_1:def_3;
then A7: i in (dom M1) /\ (dom M2) by PRE_POLY:def_4;
then  i in dom M1 by XBOOLE_0:def_4;
then  i in Seg (len M1) by FINSEQ_1:def_3;
then  i in Seg (len (Sum M1)) by Def1;
then A8: i in dom (Sum M1) by FINSEQ_1:def_3;
 i in dom M2 by A7, XBOOLE_0:def_4;
then  i in Seg (len M2) by FINSEQ_1:def_3;
then  i in Seg (len (Sum M2)) by Def1;
then A9: i in dom (Sum M2) by FINSEQ_1:def_3;
A10: i in dom (Sum (M1 ^^ M2)) by A2, A3, A4, FINSEQ_1:def_3;
A11: (M1 . i) ^ (M2 . i) = (M1 ^^ M2) . i by A6, PRE_POLY:def_4;
thus ((Sum M1) + (Sum M2)) . i = (addreal .: ((Sum M1),(Sum M2))) . i
.= addreal . (((Sum M1) . i),((Sum M2) . i)) by A5, FUNCOP_1:22
.= ((Sum M1) . i) + ((Sum M2) . i) by BINOP_2:def_9
.= (Sum (M1 . i)) + ((Sum M2) . i) by A8, Def1
.= (Sum (M1 . i)) + (Sum (M2 . i)) by A9, Def1
.= Sum ((M1 ^^ M2) . i) by A11, RVSUM_1:75
.= (Sum (M1 ^^ M2)) . i by A10, Def1 ; ::_thesis: verum
end;
hence  (Sum M1) + (Sum M2) = Sum (M1 ^^ M2) by A2, FINSEQ_2:9; ::_thesis: verum
end;

theorem Th27: :: MATRPROB:27
for M1, M2 being Matrix of REAL st len M1 = len M2 holds
(SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2)
proof
let M1, M2 be Matrix of REAL; ::_thesis: ( len M1 = len M2 implies (SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2) )
assume A1: len M1 = len M2 ; ::_thesis: (SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2)
len (Sum M1) = len M1 by Def1
.= len (Sum M2) by A1, Def1 ;
then reconsider p1 = Sum M1, p2 = Sum M2 as Element of (len (Sum M1)) -tuples_on REAL by FINSEQ_2:92;
thus (SumAll M1) + (SumAll M2) = Sum (p1 + p2) by RVSUM_1:89
.= SumAll (M1 ^^ M2) by Th26 ; ::_thesis: verum
end;

theorem Th28: :: MATRPROB:28
for M being Matrix of REAL holds SumAll M = SumAll (M @)
proof
let M be Matrix of REAL; ::_thesis: SumAll M = SumAll (M @)
defpred S1[ Nat] means  for M being Matrix of REAL st len M = $1 holds
SumAll M = SumAll (M @);
A1: for p being FinSequence of REAL holds SumAll <*p*> = SumAll (<*p*> @)
proof
defpred S2[ FinSequence of REAL ] means  SumAll <*$1*> = SumAll (<*$1*> @);
let p be FinSequence of REAL ; ::_thesis: SumAll <*p*> = SumAll (<*p*> @)
A2: for p being FinSequence of REAL
for x being Element of REAL st S2[p] holds
S2[p ^ <*x*>]
proof
let p be FinSequence of REAL ; ::_thesis: for x being Element of REAL st S2[p] holds
S2[p ^ <*x*>]
let x be Element of REAL ; ::_thesis: ( S2[p] implies S2[p ^ <*x*>] )
assume A3: SumAll <*p*> = SumAll (<*p*> @) ; ::_thesis: S2[p ^ <*x*>]
Seg (len (<*p*> ^^ <*<*x*>*>)) = dom (<*p*> ^^ <*<*x*>*>) by FINSEQ_1:def_3
.= (dom <*p*>) /\ (dom <*<*x*>*>) by PRE_POLY:def_4
.= (Seg 1) /\ (dom <*<*x*>*>) by FINSEQ_1:38
.= (Seg 1) /\ (Seg 1) by FINSEQ_1:38
.= Seg 1 ;
then A4: len (<*p*> ^^ <*<*x*>*>) = 1 by FINSEQ_1:6
.= len <*(p ^ <*x*>)*> by FINSEQ_1:39 ;
A5: dom <*(p ^ <*x*>)*> = Seg (len <*(p ^ <*x*>)*>) by FINSEQ_1:def_3;
A6: now__::_thesis:_for_i_being_Nat_st_i_in_dom_<*(p_^_<*x*>)*>_holds_
(<*p*>_^^_<*<*x*>*>)_._i_=_<*(p_^_<*x*>)*>_._i
let i be Nat; ::_thesis: ( i in dom <*(p ^ <*x*>)*> implies (<*p*> ^^ <*<*x*>*>) . i = <*(p ^ <*x*>)*> . i )
reconsider M1 = <*p*> . i, M2 = <*<*x*>*> . i as FinSequence ;
assume A7: i in dom <*(p ^ <*x*>)*> ; ::_thesis: (<*p*> ^^ <*<*x*>*>) . i = <*(p ^ <*x*>)*> . i
then  i in {1} by A5, FINSEQ_1:2, FINSEQ_1:40;
then A8: i = 1 by TARSKI:def_1;
 i in dom (<*p*> ^^ <*<*x*>*>) by A4, A5, A7, FINSEQ_1:def_3;
hence (<*p*> ^^ <*<*x*>*>) . i = M1 ^ M2 by PRE_POLY:def_4
.= p ^ M2 by A8, FINSEQ_1:40
.= p ^ <*x*> by A8, FINSEQ_1:40
.= <*(p ^ <*x*>)*> . i by A8, FINSEQ_1:40 ;
::_thesis: verum
end;
percases ( len p = 0 or len p <> 0 ) ;
suppose len p = 0 ; ::_thesis: S2[p ^ <*x*>]
then A9: p = {} ;
hence  SumAll <*(p ^ <*x*>)*> = SumAll <*<*x*>*> by FINSEQ_1:34
.= SumAll (<*<*x*>*> @) by MATRLIN:15
.= SumAll (<*(p ^ <*x*>)*> @) by A9, FINSEQ_1:34 ;
::_thesis: verum
end;
supposeA10: len p <> 0 ; ::_thesis: S2[p ^ <*x*>]
A11: len <*<*x*>*> = 1 by FINSEQ_1:40;
then A12: width <*<*x*>*> = len <*x*> by MATRIX_1:20
.= 1 by FINSEQ_1:40 ;
then A13: len (<*<*x*>*> @) = 1 by MATRIX_1:def_6;
A14: len <*p*> = 1 by FINSEQ_1:40;
then A15: width <*p*> = len p by MATRIX_1:20;
then A16: len (<*p*> @) = len p by MATRIX_1:def_6;
 width (<*p*> @) = 1 by A10, A14, A15, MATRIX_2:10;
then reconsider d1 = <*p*> @ as Matrix of len p,1, REAL by A10, A16, MATRIX_1:20;
A17: len <*(p ^ <*x*>)*> = 1 by FINSEQ_1:40;
then A18: width <*(p ^ <*x*>)*> = len (p ^ <*x*>) by MATRIX_1:20
.= (len p) + (len <*x*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
A19: (<*<*x*>*> @) @ = <*<*x*>*> by A11, A12, MATRIX_2:13;
A20: width (<*p*> @) = len <*p*> by A10, A15, MATRIX_2:10
.= width (<*<*x*>*> @) by A14, A11, A12, MATRIX_2:10 ;
then  width (<*<*x*>*> @) = 1 by A10, A14, A15, MATRIX_2:10;
then reconsider d2 = <*<*x*>*> @ as Matrix of 1,1, REAL by A13, MATRIX_1:20;
A21: (d1 ^ d2) @ = ((<*p*> @) @) ^^ ((<*<*x*>*> @) @) by A20, MATRLIN:28
.= <*p*> ^^ <*<*x*>*> by A10, A14, A15, A19, MATRIX_2:13
.= <*(p ^ <*x*>)*> by A4, A6, FINSEQ_2:9
.= (<*(p ^ <*x*>)*> @) @ by A17, A18, MATRIX_2:13 ;
A22: len ((<*p*> @) ^ (<*<*x*>*> @)) = (len (<*p*> @)) + (len (<*<*x*>*> @)) by FINSEQ_1:22
.= (width <*p*>) + (len (<*<*x*>*> @)) by MATRIX_1:def_6
.= (width <*p*>) + (width <*<*x*>*>) by MATRIX_1:def_6
.= len (<*(p ^ <*x*>)*> @) by A15, A12, A18, MATRIX_1:def_6 ;
thus  SumAll <*(p ^ <*x*>)*> = SumAll (<*p*> ^^ <*<*x*>*>) by A4, A6, FINSEQ_2:9
.= (SumAll (<*p*> @)) + (SumAll <*<*x*>*>) by A3, A14, A11, Th27
.= (SumAll (<*p*> @)) + (SumAll (<*<*x*>*> @)) by MATRLIN:15
.= Sum ((Sum d1) ^ (Sum d2)) by RVSUM_1:75
.= SumAll (d1 ^ d2) by Th25
.= SumAll (<*(p ^ <*x*>)*> @) by A22, A21, MATRIX_2:9 ; ::_thesis: verum
end;
end;
end;
A23: S2[ <*> REAL]
proof
reconsider M1 = <*(<*> REAL)*> as Matrix of 1, 0 , REAL ;
 len M1 = 1 by MATRIX_1:def_2;
then  width M1 = 0 by MATRIX_1:20;
then A24: len (M1 @) = 0 by MATRIX_1:def_6;
SumAll M1 = 0 by Th24
.= SumAll (M1 @) by A24, Th23 ;
hence  S2[ <*> REAL] ; ::_thesis: verum
end;
 for p being FinSequence of REAL holds S2[p] from FINSEQ_2:sch_2(A23, A2);
hence  SumAll <*p*> = SumAll (<*p*> @) ; ::_thesis: verum
end;
A25: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A26: for M being Matrix of REAL st len M = n holds
SumAll M = SumAll (M @) ; ::_thesis: S1[n + 1]
thus  for M being Matrix of REAL st len M = n + 1 holds
SumAll M = SumAll (M @) ::_thesis: verum
proof
let M be Matrix of REAL; ::_thesis: ( len M = n + 1 implies SumAll M = SumAll (M @) )
assume A27: len M = n + 1 ; ::_thesis: SumAll M = SumAll (M @)
A28: dom M = Seg (len M) by FINSEQ_1:def_3;
percases ( n = 0 or n > 0 ) ;
supposeA29: n = 0 ; ::_thesis: SumAll M = SumAll (M @)
reconsider g = M . 1 as FinSequence of REAL ;
 M = <*g*> by A27, A29, FINSEQ_1:40;
hence  SumAll M = SumAll (M @) by A1; ::_thesis: verum
end;
supposeA30: n > 0 ; ::_thesis: SumAll M = SumAll (M @)
reconsider M9 = M as Matrix of n + 1, width M, REAL by A27, MATRIX_1:20;
reconsider M1 = M . (n + 1) as FinSequence of REAL ;
reconsider w = Del (M9,(n + 1)) as Matrix of n, width M, REAL by MATRLIN:3;
 M . (n + 1) = Line (M,(n + 1)) by A27, A28, FINSEQ_1:4, MATRIX_2:16;
then reconsider r = <*M1*> as Matrix of 1, width M, REAL by MATRIX_1:def_7;
A31: width w = width M9 by A30, MATRLIN:2
.= width r by MATRLIN:2 ;
A32: len (w @) = width w by MATRIX_1:def_6
.= len (r @) by A31, MATRIX_1:def_6 ;
A33: len (Del (M,(n + 1))) = n by A27, PRE_POLY:12;
thus  SumAll M = SumAll (w ^ r) by A27, PRE_POLY:13
.= Sum ((Sum w) ^ (Sum r)) by Th25
.= (SumAll (Del (M,(n + 1)))) + (SumAll r) by RVSUM_1:75
.= (SumAll ((Del (M,(n + 1))) @)) + (SumAll r) by A26, A33
.= (SumAll ((Del (M,(n + 1))) @)) + (SumAll (r @)) by A1
.= SumAll ((w @) ^^ (r @)) by A32, Th27
.= SumAll ((w ^ r) @) by A31, MATRLIN:28
.= SumAll (M @) by A27, PRE_POLY:13 ; ::_thesis: verum
end;
end;
end;
end;
A34: S1[ 0 ]
proof
let M be Matrix of REAL; ::_thesis: ( len M = 0 implies SumAll M = SumAll (M @) )
assume A35: len M = 0 ; ::_thesis: SumAll M = SumAll (M @)
then  width M = 0 by MATRIX_1:def_3;
then A36: len (M @) = 0 by MATRIX_1:def_6;
thus  SumAll M = 0 by A35, Th23
.= SumAll (M @) by A36, Th23 ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A34, A25);
then  S1[ len M] ;
hence  SumAll M = SumAll (M @) ; ::_thesis: verum
end;

theorem Th29: :: MATRPROB:29
for M being Matrix of REAL holds SumAll M = Sum (ColSum M)
proof
let M be Matrix of REAL; ::_thesis: SumAll M = Sum (ColSum M)
thus  Sum (ColSum M) = SumAll (M @) by Th22
.= SumAll M by Th28 ; ::_thesis: verum
end;

theorem Th30: :: MATRPROB:30
for x, y being FinSequence of REAL st len x = len y holds
len (mlt (x,y)) = len x by FINSEQ_2:72;

theorem Th31: :: MATRPROB:31
for i being Element of NAT
for R being Element of i -tuples_on REAL holds mlt ((i |-> 1),R) = R
proof
let i be Element of NAT ; ::_thesis: for R being Element of i -tuples_on REAL holds mlt ((i |-> 1),R) = R
let R be Element of i -tuples_on REAL; ::_thesis: mlt ((i |-> 1),R) = R
thus  mlt ((i |-> 1),R) = 1 * R by RVSUM_1:63
.= R by RVSUM_1:52 ; ::_thesis: verum
end;

theorem Th32: :: MATRPROB:32
for x being FinSequence of REAL holds mlt (((len x) |-> 1),x) = x
proof
let x be FinSequence of REAL ; ::_thesis: mlt (((len x) |-> 1),x) = x
reconsider y = x as Element of (len x) -tuples_on REAL by FINSEQ_2:92;
 mlt (((len x) |-> 1),y) = y by Th31;
hence  mlt (((len x) |-> 1),x) = x ; ::_thesis: verum
end;

theorem Th33: :: MATRPROB:33
for x, y being FinSequence of REAL st ( for i being Element of NAT st i in dom x holds
x . i >= 0 ) & ( for i being Element of NAT st i in dom y holds
y . i >= 0 ) holds
for k being Element of NAT st k in dom (mlt (x,y)) holds
(mlt (x,y)) . k >= 0
proof
A1: for z being FinSequence of REAL st ( for i being Element of NAT st i in dom z holds
z . i >= 0 ) holds
for i being Element of NAT holds z . i >= 0
proof
let z be FinSequence of REAL ; ::_thesis: ( ( for i being Element of NAT st i in dom z holds
z . i >= 0 ) implies for i being Element of NAT holds z . i >= 0 )
assume A2: for i being Element of NAT st i in dom z holds
z . i >= 0 ; ::_thesis: for i being Element of NAT holds z . i >= 0
hereby  ::_thesis: verum
let i be Element of NAT ; ::_thesis: z . b1 >= 0
percases ( not i in dom z or i in dom z ) ;
suppose not i in dom z ; ::_thesis: z . b1 >= 0
hence  z . i >= 0 by FUNCT_1:def_2; ::_thesis: verum
end;
suppose i in dom z ; ::_thesis: z . b1 >= 0
hence  z . i >= 0 by A2; ::_thesis: verum
end;
end;
end;
end;
let x, y be FinSequence of REAL ; ::_thesis: ( ( for i being Element of NAT st i in dom x holds
x . i >= 0 ) & ( for i being Element of NAT st i in dom y holds
y . i >= 0 ) implies for k being Element of NAT st k in dom (mlt (x,y)) holds
(mlt (x,y)) . k >= 0 )
assume A3: ( ( for i being Element of NAT st i in dom x holds
x . i >= 0 ) & ( for i being Element of NAT st i in dom y holds
y . i >= 0 ) ) ; ::_thesis: for k being Element of NAT st k in dom (mlt (x,y)) holds
(mlt (x,y)) . k >= 0
hereby  ::_thesis: verum
let k be Element of NAT ; ::_thesis: ( k in dom (mlt (x,y)) implies (mlt (x,y)) . k >= 0 )
assume  k in dom (mlt (x,y)) ; ::_thesis: (mlt (x,y)) . k >= 0
A4: (mlt (x,y)) . k = (x . k) * (y . k) by RVSUM_1:59;
 ( x . k >= 0 & y . k >= 0 ) by A3, A1;
hence  (mlt (x,y)) . k >= 0 by A4, XREAL_1:127; ::_thesis: verum
end;
end;

theorem Th34: :: MATRPROB:34
for i being Element of NAT
for e1, e2 being Element of i -tuples_on REAL
for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 & e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)
proof
let i be Element of NAT ; ::_thesis: for e1, e2 being Element of i -tuples_on REAL
for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 & e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)
let e1, e2 be Element of i -tuples_on REAL; ::_thesis: for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 & e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)
let f1, f2 be Element of i -tuples_on the carrier of F_Real; ::_thesis: ( e1 = f1 & e2 = f2 implies mlt (e1,e2) = mlt (f1,f2) )
assume A1: ( e1 = f1 & e2 = f2 ) ; ::_thesis: mlt (e1,e2) = mlt (f1,f2)
A2: dom (mlt (e1,e2)) = Seg (len (mlt (e1,e2))) by FINSEQ_1:def_3
.= Seg i by CARD_1:def_7
.= Seg (len (mlt (f1,f2))) by CARD_1:def_7
.= dom (mlt (f1,f2)) by FINSEQ_1:def_3 ;
 for i being Nat st i in dom (mlt (e1,e2)) holds
(mlt (e1,e2)) . i = (mlt (f1,f2)) . i
proof
let i be Nat; ::_thesis: ( i in dom (mlt (e1,e2)) implies (mlt (e1,e2)) . i = (mlt (f1,f2)) . i )
assume A3: i in dom (mlt (e1,e2)) ; ::_thesis: (mlt (e1,e2)) . i = (mlt (f1,f2)) . i
reconsider a1 = e1 . i, a2 = e2 . i as Element of F_Real by VECTSP_1:def_5;
thus (mlt (e1,e2)) . i = a1 * a2 by RVSUM_1:59
.= (mlt (f1,f2)) . i by A1, A2, A3, FVSUM_1:60 ; ::_thesis: verum
end;
hence  mlt (e1,e2) = mlt (f1,f2) by A2, FINSEQ_1:13; ::_thesis: verum
end;

theorem Th35: :: MATRPROB:35
for e1, e2 being FinSequence of REAL
for f1, f2 being FinSequence of F_Real st len e1 = len e2 & e1 = f1 & e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)
proof
let e1, e2 be FinSequence of REAL ; ::_thesis: for f1, f2 being FinSequence of F_Real st len e1 = len e2 & e1 = f1 & e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)
let f1, f2 be FinSequence of F_Real; ::_thesis: ( len e1 = len e2 & e1 = f1 & e2 = f2 implies mlt (e1,e2) = mlt (f1,f2) )
assume that
A1: len e1 = len e2 and
A2: e1 = f1 and
A3: e2 = f2 ; ::_thesis: mlt (e1,e2) = mlt (f1,f2)
set l = len e1;
set Z =  {  f where f is Element of the carrier of F_Real * : len f = len e1  }  ;
 f1 is Element of the carrier of F_Real * by FINSEQ_1:def_11;
then  f1 in  {  f where f is Element of the carrier of F_Real * : len f = len e1  }  by A2;
then reconsider f3 = f1 as Element of (len e1) -tuples_on the carrier of F_Real ;
 f2 is Element of the carrier of F_Real * by FINSEQ_1:def_11;
then  f2 in  {  f where f is Element of the carrier of F_Real * : len f = len e1  }  by A1, A3;
then reconsider f4 = f2 as Element of (len e1) -tuples_on the carrier of F_Real ;
set Y =  {  e where e is Element of REAL * : len e = len e1  }  ;
 e2 is Element of REAL * by FINSEQ_1:def_11;
then  e2 in  {  e where e is Element of REAL * : len e = len e1  }  by A1;
then reconsider e4 = e2 as Element of (len e1) -tuples_on REAL ;
reconsider e3 = e1 as Element of (len e1) -tuples_on REAL by FINSEQ_2:92;
 mlt (e3,e4) = mlt (f3,f4) by A2, A3, Th34;
hence  mlt (e1,e2) = mlt (f1,f2) ; ::_thesis: verum
end;

theorem Th36: :: MATRPROB:36
for e being FinSequence of REAL
for f being FinSequence of F_Real st e = f holds
Sum e = Sum f
proof
let e be FinSequence of REAL ; ::_thesis: for f being FinSequence of F_Real st e = f holds
Sum e = Sum f
let f be FinSequence of F_Real; ::_thesis: ( e = f implies Sum e = Sum f )
assume A1: e = f ; ::_thesis: Sum e = Sum f
consider e1 being Function of NAT,REAL such that
A2: e1 . 0 = 0 and
A3: for i being Nat st i < len e holds
e1 . (i + 1) = (e1 . i) + (e . (i + 1)) and
A4: Sum e = e1 . (len e) by Th7;
consider f1 being Function of NAT, the carrier of F_Real such that
A5: Sum f = f1 . (len f) and
A6: f1 . 0 = 0. F_Real and
A7: for j being Element of NAT
for v being Element of F_Real st j < len f & v = f . (j + 1) holds
f1 . (j + 1) = (f1 . j) + v by RLVECT_1:def_12;
 for n being Nat st n <= len e holds
e1 . n = f1 . n
proof
defpred S1[ Nat] means ( $1 <= len e implies e1 . $1 = f1 . $1 );
let n be Nat; ::_thesis: ( n <= len e implies e1 . n = f1 . n )
A8: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_(_k_+_1_<=_len_e_implies_e1_._(k_+_1)_=_f1_._(k_+_1)_)
reconsider k9 = k as Element of NAT by ORDINAL1:def_12;
reconsider a = e . (k + 1) as Element of F_Real by VECTSP_1:def_5;
assume  k + 1 <= len e ; ::_thesis: e1 . (k + 1) = f1 . (k + 1)
then A10: k < len e by NAT_1:13;
then e1 . (k + 1) = (f1 . k9) + a by A3, A9
.= f1 . (k + 1) by A1, A7, A10 ;
hence  e1 . (k + 1) = f1 . (k + 1) ; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A11: S1[ 0 ] by A2, A6, STRUCT_0:def_6, VECTSP_1:def_5;
 for n being Nat holds S1[n] from NAT_1:sch_2(A11, A8);
hence  ( n <= len e implies e1 . n = f1 . n ) ; ::_thesis: verum
end;
hence  Sum e = Sum f by A1, A4, A5; ::_thesis: verum
end;

notation
let e1, e2 be FinSequence of REAL ;
synonym e1 "*" e2 for |(e1,e2)|;
end;

theorem :: MATRPROB:37
for i being Element of NAT
for e1, e2 being Element of i -tuples_on REAL
for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 & e2 = f2 holds
e1 "*" e2 = f1 "*" f2
proof
let i be Element of NAT ; ::_thesis: for e1, e2 being Element of i -tuples_on REAL
for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 & e2 = f2 holds
e1 "*" e2 = f1 "*" f2
let e1, e2 be Element of i -tuples_on REAL; ::_thesis: for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 & e2 = f2 holds
e1 "*" e2 = f1 "*" f2
let f1, f2 be Element of i -tuples_on the carrier of F_Real; ::_thesis: ( e1 = f1 & e2 = f2 implies e1 "*" e2 = f1 "*" f2 )
assume  ( e1 = f1 & e2 = f2 ) ; ::_thesis: e1 "*" e2 = f1 "*" f2
hence e1 "*" e2 = Sum (mlt (f1,f2)) by Th34, Th36
.= f1 "*" f2 by FVSUM_1:def_9 ;
::_thesis: verum
end;

theorem Th38: :: MATRPROB:38
for e1, e2 being FinSequence of REAL
for f1, f2 being FinSequence of F_Real st len e1 = len e2 & e1 = f1 & e2 = f2 holds
e1 "*" e2 = f1 "*" f2
proof
let e1, e2 be FinSequence of REAL ; ::_thesis: for f1, f2 being FinSequence of F_Real st len e1 = len e2 & e1 = f1 & e2 = f2 holds
e1 "*" e2 = f1 "*" f2
let f1, f2 be FinSequence of F_Real; ::_thesis: ( len e1 = len e2 & e1 = f1 & e2 = f2 implies e1 "*" e2 = f1 "*" f2 )
assume  ( len e1 = len e2 & e1 = f1 & e2 = f2 ) ; ::_thesis: e1 "*" e2 = f1 "*" f2
hence e1 "*" e2 = Sum (mlt (f1,f2)) by Th35, Th36
.= f1 "*" f2 by FVSUM_1:def_9 ;
::_thesis: verum
end;

theorem Th39: :: MATRPROB:39
for M, M1, M2 being Matrix of REAL st width M1 = len M2 holds
( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) ) )
proof
let M, M1, M2 be Matrix of REAL; ::_thesis: ( width M1 = len M2 implies ( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) ) ) )
assume A1: width M1 = len M2 ; ::_thesis: ( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) ) )
set MM = MXR2MXF M;
set M4 = MXR2MXF M2;
set M3 = MXR2MXF M1;
A2: MXR2MXF M1 = M1 by MATRIXR1:def_1;
A3: MXR2MXF M2 = M2 by MATRIXR1:def_1;
 MXF2MXR ((MXR2MXF M1) * (MXR2MXF M2)) = M1 * M2 by MATRIXR1:def_6;
then A4: (MXR2MXF M1) * (MXR2MXF M2) = M1 * M2 by MATRIXR1:def_2;
hereby  ::_thesis: ( len M = len M1 & width M = width M2 & ( for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) implies M = M1 * M2 )
assume A5: M = M1 * M2 ; ::_thesis: ( len M = len M1 & width M = width M2 & ( for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) )
hence A6: len M = len M1 by A1, A2, A3, A4, MATRIX_3:def_4; ::_thesis: ( width M = width M2 & ( for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) )
thus A7: width M = width M2 by A1, A2, A3, A4, A5, MATRIX_3:def_4; ::_thesis: for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j))
thus  for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ::_thesis: verum
proof
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices M implies M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) )
assume A8: [i,j] in Indices M ; ::_thesis: M * (i,j) = (Line (M1,i)) "*" (Col (M2,j))
 j in Seg (width M2) by A7, A8, Th12;
then A9: Col ((MXR2MXF M2),j) = Col (M2,j) by A3, Th17;
 i in Seg (len M1) by A6, A8, Th12;
then  i in dom M1 by FINSEQ_1:def_3;
then A10: Line ((MXR2MXF M1),i) = Line (M1,i) by A2, Th16;
A11: len (Line (M1,i)) = width M1 by MATRIX_1:def_7
.= len (Col (M2,j)) by A1, MATRIX_1:def_8 ;
 M = MXF2MXR ((MXR2MXF M1) * (MXR2MXF M2)) by A5, MATRIXR1:def_6;
then  ( [i,j] in Indices ((MXR2MXF M1) * (MXR2MXF M2)) & M * (i,j) = ((MXR2MXF M1) * (MXR2MXF M2)) * (i,j) ) by A8, MATRIXR1:23, MATRIXR1:def_2;
hence M * (i,j) = (Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j)) by A1, A2, A3, MATRIX_3:def_4
.= (Line (M1,i)) "*" (Col (M2,j)) by A10, A9, A11, Th38 ;
::_thesis: verum
end;
end;
assume that
A12: len M = len M1 and
A13: width M = width M2 and
A14: for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ; ::_thesis: M = M1 * M2
A15: width (MXR2MXF M) = width M by MATRIXR1:def_1
.= width (MXR2MXF M2) by A13, MATRIXR1:def_1 ;
A16: len (MXR2MXF M) = len M by MATRIXR1:def_1
.= len (MXR2MXF M1) by A12, MATRIXR1:def_1 ;
 for i, j being Nat st [i,j] in Indices (MXR2MXF M) holds
(MXR2MXF M) * (i,j) = (Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (MXR2MXF M) implies (MXR2MXF M) * (i,j) = (Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j)) )
assume A17: [i,j] in Indices (MXR2MXF M) ; ::_thesis: (MXR2MXF M) * (i,j) = (Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j))
A18: ( i in NAT & j in NAT ) by ORDINAL1:def_12;
then  j in Seg (width (MXR2MXF M2)) by A15, A17, Th12;
then A19: Col ((MXR2MXF M2),j) = Col (M2,j) by Th17, MATRIXR1:def_1;
 i in Seg (len (MXR2MXF M1)) by A16, A17, A18, Th12;
then  i in dom (MXR2MXF M1) by FINSEQ_1:def_3;
then A20: Line ((MXR2MXF M1),i) = Line (M1,i) by Th16, MATRIXR1:def_1;
A21: len (Line (M1,i)) = width M1 by MATRIX_1:def_7
.= len (Col (M2,j)) by A1, MATRIX_1:def_8 ;
 ( [i,j] in Indices M & (MXR2MXF M) * (i,j) = M * (i,j) ) by A17, MATRIXR1:23, MATRIXR1:def_1;
hence (MXR2MXF M) * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) by A14, A18
.= (Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j)) by A20, A19, A21, Th38 ;
::_thesis: verum
end;
then  ( MXR2MXF M = M & MXR2MXF M = (MXR2MXF M1) * (MXR2MXF M2) ) by A1, A2, A3, A16, A15, MATRIXR1:def_1, MATRIX_3:def_4;
then  M = MXF2MXR ((MXR2MXF M1) * (MXR2MXF M2)) by MATRIXR1:def_2;
hence  M = M1 * M2 by MATRIXR1:def_6; ::_thesis: verum
end;

theorem Th40: :: MATRPROB:40
for M being Matrix of REAL
for p being FinSequence of REAL st len M = len p holds
for i being Element of NAT st i in Seg (len (p * M)) holds
(p * M) . i = p "*" (Col (M,i))
proof
let M be Matrix of REAL; ::_thesis: for p being FinSequence of REAL st len M = len p holds
for i being Element of NAT st i in Seg (len (p * M)) holds
(p * M) . i = p "*" (Col (M,i))
let p be FinSequence of REAL ; ::_thesis: ( len M = len p implies for i being Element of NAT st i in Seg (len (p * M)) holds
(p * M) . i = p "*" (Col (M,i)) )
assume A1: len M = len p ; ::_thesis: for i being Element of NAT st i in Seg (len (p * M)) holds
(p * M) . i = p "*" (Col (M,i))
A2: len (p * M) = len (Line (((LineVec2Mx p) * M),1)) by MATRIXR1:def_12
.= width ((LineVec2Mx p) * M) by MATRIX_1:def_7 ;
hereby  ::_thesis: verum
let i be Element of NAT ; ::_thesis: ( i in Seg (len (p * M)) implies p "*" (Col (M,i)) = (p * M) . i )
assume A3: i in Seg (len (p * M)) ; ::_thesis: p "*" (Col (M,i)) = (p * M) . i
A4: width (LineVec2Mx p) = len M by A1, MATRIXR1:def_10;
then  len ((LineVec2Mx p) * M) = len (LineVec2Mx p) by Th39;
then  len ((LineVec2Mx p) * M) = 1 by MATRIXR1:48;
then  1 in Seg (len ((LineVec2Mx p) * M)) by FINSEQ_1:1;
then  [1,i] in Indices ((LineVec2Mx p) * M) by A2, A3, Th12;
then A5: ((LineVec2Mx p) * M) * (1,i) = (Line ((LineVec2Mx p),1)) "*" (Col (M,i)) by A4, Th39
.= p "*" (Col (M,i)) by MATRIXR1:48 ;
 (Line (((LineVec2Mx p) * M),1)) . i = ((LineVec2Mx p) * M) * (1,i) by A2, A3, MATRIX_1:def_7;
hence  p "*" (Col (M,i)) = (p * M) . i by A5, MATRIXR1:def_12; ::_thesis: verum
end;
end;

theorem Th41: :: MATRPROB:41
for M being Matrix of REAL
for p being FinSequence of REAL st width M = len p & width M > 0 holds
for i being Element of NAT st i in Seg (len (M * p)) holds
(M * p) . i = (Line (M,i)) "*" p
proof
let M be Matrix of REAL; ::_thesis: for p being FinSequence of REAL st width M = len p & width M > 0 holds
for i being Element of NAT st i in Seg (len (M * p)) holds
(M * p) . i = (Line (M,i)) "*" p
let p be FinSequence of REAL ; ::_thesis: ( width M = len p & width M > 0 implies for i being Element of NAT st i in Seg (len (M * p)) holds
(M * p) . i = (Line (M,i)) "*" p )
assume A1: ( width M = len p & width M > 0 ) ; ::_thesis: for i being Element of NAT st i in Seg (len (M * p)) holds
(M * p) . i = (Line (M,i)) "*" p
A2: len (M * p) = len (Col ((M * (ColVec2Mx p)),1)) by MATRIXR1:def_11
.= len (M * (ColVec2Mx p)) by MATRIX_1:def_8 ;
hereby  ::_thesis: verum
let i be Element of NAT ; ::_thesis: ( i in Seg (len (M * p)) implies (Line (M,i)) "*" p = (M * p) . i )
assume A3: i in Seg (len (M * p)) ; ::_thesis: (Line (M,i)) "*" p = (M * p) . i
 i in dom (M * (ColVec2Mx p)) by A2, A3, FINSEQ_1:def_3;
then A4: (Col ((M * (ColVec2Mx p)),1)) . i = (M * (ColVec2Mx p)) * (i,1) by MATRIX_1:def_8;
A5: len (ColVec2Mx p) = width M by A1, MATRIXR1:def_9;
then  width (M * (ColVec2Mx p)) = width (ColVec2Mx p) by Th39;
then  width (M * (ColVec2Mx p)) = 1 by A1, MATRIXR1:def_9;
then  1 in Seg (width (M * (ColVec2Mx p))) by FINSEQ_1:1;
then  [i,1] in Indices (M * (ColVec2Mx p)) by A2, A3, Th12;
then (M * (ColVec2Mx p)) * (i,1) = (Line (M,i)) "*" (Col ((ColVec2Mx p),1)) by A5, Th39
.= (Line (M,i)) "*" p by A1, MATRIXR1:45 ;
hence  (Line (M,i)) "*" p = (M * p) . i by A4, MATRIXR1:def_11; ::_thesis: verum
end;
end;

theorem Th42: :: MATRPROB:42
for M, M1, M2 being Matrix of REAL st width M1 = len M2 holds
( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i being Element of NAT st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ) ) )
proof
let M, M1, M2 be Matrix of REAL; ::_thesis: ( width M1 = len M2 implies ( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i being Element of NAT st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ) ) ) )
assume A1: width M1 = len M2 ; ::_thesis: ( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i being Element of NAT st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ) ) )
hereby  ::_thesis: ( len M = len M1 & width M = width M2 & ( for i being Element of NAT st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ) implies M = M1 * M2 )
assume A2: M = M1 * M2 ; ::_thesis: ( len M = len M1 & width M = width M2 & ( for i being Element of NAT st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ) )
hence A3: ( len M = len M1 & width M = width M2 ) by A1, Th39; ::_thesis: for i being Element of NAT st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2
thus  for i being Element of NAT st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( i in Seg (len M) implies Line (M,i) = (Line (M1,i)) * M2 )
assume A4: i in Seg (len M) ; ::_thesis: Line (M,i) = (Line (M1,i)) * M2
A5: len (Line (M1,i)) = len M2 by A1, MATRIX_1:def_7;
then A6: len ((Line (M1,i)) * M2) = width M2 by MATRIXR1:62;
 len (Line (M,i)) = width M by MATRIX_1:def_7;
then A7: dom (Line (M,i)) = Seg (width M2) by A3, FINSEQ_1:def_3
.= dom ((Line (M1,i)) * M2) by A6, FINSEQ_1:def_3 ;
A8: i in dom M by A4, FINSEQ_1:def_3;
 for j being Nat st j in dom (Line (M,i)) holds
(Line (M,i)) . j = ((Line (M1,i)) * M2) . j
proof
let j be Nat; ::_thesis: ( j in dom (Line (M,i)) implies (Line (M,i)) . j = ((Line (M1,i)) * M2) . j )
assume A9: j in dom (Line (M,i)) ; ::_thesis: (Line (M,i)) . j = ((Line (M1,i)) * M2) . j
A10: j in Seg (len ((Line (M1,i)) * M2)) by A7, A9, FINSEQ_1:def_3;
 j in Seg (len (Line (M,i))) by A9, FINSEQ_1:def_3;
then  j in Seg (width M) by MATRIX_1:def_7;
then A11: [i,j] in Indices M by A4, Th12;
thus (Line (M,i)) . j = (M . i) . j by A8, MATRIX_2:16
.= M * (i,j) by A11, MATRIX_1:def_5
.= (Line (M1,i)) "*" (Col (M2,j)) by A1, A2, A9, A11, Th39
.= ((Line (M1,i)) * M2) . j by A5, A10, Th40 ; ::_thesis: verum
end;
hence  Line (M,i) = (Line (M1,i)) * M2 by A7, FINSEQ_1:13; ::_thesis: verum
end;
end;
assume that
A12: len M = len M1 and
A13: width M = width M2 and
A14: for i being Element of NAT st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ; ::_thesis: M = M1 * M2
 for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j))
proof
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices M implies M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) )
assume A15: [i,j] in Indices M ; ::_thesis: M * (i,j) = (Line (M1,i)) "*" (Col (M2,j))
A16: i in Seg (len M) by A15, Th12;
then A17: i in dom M by FINSEQ_1:def_3;
A18: len (Line (M1,i)) = len M2 by A1, MATRIX_1:def_7;
 j in Seg (width M) by A15, Th12;
then A19: j in Seg (len ((Line (M1,i)) * M2)) by A13, A18, MATRIXR1:62;
thus M * (i,j) = (M . i) . j by A15, MATRIX_1:def_5
.= (Line (M,i)) . j by A17, MATRIX_2:16
.= ((Line (M1,i)) * M2) . j by A14, A16
.= (Line (M1,i)) "*" (Col (M2,j)) by A18, A19, Th40 ; ::_thesis: verum
end;
hence  M = M1 * M2 by A1, A12, A13, Th39; ::_thesis: verum
end;

definition
let x, y be FinSequence of REAL ;
let M be Matrix of REAL;
assume that
A1: len x = len M and
A2: len y = width M ;
func QuadraticForm (x,M,y) ->  Matrix of REAL means :Def4: :: MATRPROB:def 4
( len it = len x & width it = len y & ( for i, j being Nat st [i,j] in Indices M holds
it * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) );
existence
 ex b1 being Matrix of REAL st
( len b1 = len x & width b1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) )
proof
deffunc H1( Nat, Nat) ->  Element of REAL = ((x . $1) * (M * ($1,$2))) * (y . $2);
consider M1 being Matrix of len M, width M, REAL  such that
A3: 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 x & width M1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) )
A4: len M1 = len x by A1, MATRIX_1:def_2;
A5: now__::_thesis:_(_(_len_M_=_0_&_width_M1_=_len_y_)_or_(_len_M_>_0_&_width_M1_=_len_y_)_)
percases ( len M = 0 or len M > 0 ) ;
caseA6: len M = 0 ; ::_thesis: width M1 = len y
then  width M1 = 0 by A1, A4, MATRIX_1:def_3;
hence  width M1 = len y by A2, A6, MATRIX_1:def_3; ::_thesis: verum
end;
case len M > 0 ; ::_thesis: width M1 = len y
hence  width M1 = len y by A2, MATRIX_1:23; ::_thesis: verum
end;
end;
end;
A7: Indices M = [:(dom M),(Seg (width M)):] by MATRIX_1:def_4;
 dom M = dom M1 by A1, A4, FINSEQ_3:29;
then  Indices M1 = [:(dom M),(Seg (width M)):] by A2, A5, MATRIX_1:def_4;
hence  ( len M1 = len x & width M1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) ) by A1, A3, A5, A7, MATRIX_1:def_2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Matrix of REAL st len b1 = len x & width b1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) & len b2 = len x & width b2 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) holds
b1 = b2
proof
let M1, M2 be Matrix of REAL; ::_thesis: ( len M1 = len x & width M1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) & len M2 = len x & width M2 = len y & ( for i, j being Nat st [i,j] in Indices M holds
M2 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) implies M1 = M2 )
assume that
A8: len M1 = len x and
A9: width M1 = len y and
A10: for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) and
A11: ( len M2 = len x & width M2 = len y ) and
A12: for i, j being Nat st [i,j] in Indices M holds
M2 * (i,j) = ((x . i) * (M * (i,j))) * (y . 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) )
A13: Indices M = [:(dom M),(Seg (width M)):] by MATRIX_1:def_4;
 dom M1 = dom M by A1, A8, FINSEQ_3:29;
then A14: Indices M1 = [:(dom M),(Seg (width M)):] by A2, A9, MATRIX_1:def_4;
assume A15: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
hence M1 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) by A10, A14, A13
.= M2 * (i,j) by A12, A15, A14, A13 ;
::_thesis: verum
end;
hence  M1 = M2 by A8, A9, A11, MATRIX_1:21; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines QuadraticForm MATRPROB:def_4_:_
 for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M & len y = width M holds
for b4 being Matrix of REAL holds
( b4 = QuadraticForm (x,M,y) iff ( len b4 = len x & width b4 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b4 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) ) );

theorem :: MATRPROB:43
for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
(QuadraticForm (x,M,y)) @ = QuadraticForm (y,(M @),x)
proof
let x, y be FinSequence of REAL ; ::_thesis: for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
(QuadraticForm (x,M,y)) @ = QuadraticForm (y,(M @),x)
let M be Matrix of REAL; ::_thesis: ( len x = len M & len y = width M & len y > 0 implies (QuadraticForm (x,M,y)) @ = QuadraticForm (y,(M @),x) )
assume that
A1: len x = len M and
A2: len y = width M and
A3: len y > 0 ; ::_thesis: (QuadraticForm (x,M,y)) @ = QuadraticForm (y,(M @),x)
A4: len (M @) = len y by A2, MATRIX_1:def_6;
A5: width (M @) = len x by A1, A2, A3, MATRIX_2:10;
then A6: ( len (QuadraticForm (y,(M @),x)) = len y & width (QuadraticForm (y,(M @),x)) = len x ) by A4, Def4;
A7: len ((QuadraticForm (x,M,y)) @) = width (QuadraticForm (x,M,y)) by MATRIX_1:def_6;
A8: width (QuadraticForm (x,M,y)) = len y by A1, A2, Def4;
then A9: width ((QuadraticForm (x,M,y)) @) = len (QuadraticForm (x,M,y)) by A3, MATRIX_2:10;
A10: for i, j being Nat st [i,j] in Indices ((QuadraticForm (x,M,y)) @) holds
(QuadraticForm (y,(M @),x)) * (i,j) = ((QuadraticForm (x,M,y)) @) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((QuadraticForm (x,M,y)) @) implies (QuadraticForm (y,(M @),x)) * (i,j) = ((QuadraticForm (x,M,y)) @) * (i,j) )
assume A11: [i,j] in Indices ((QuadraticForm (x,M,y)) @) ; ::_thesis: (QuadraticForm (y,(M @),x)) * (i,j) = ((QuadraticForm (x,M,y)) @) * (i,j)
reconsider i = i, j = j as Element of NAT by ORDINAL1:def_12;
A12: 1 <= j by A11, MATRIXC1:1;
A13: j <= len (QuadraticForm (x,M,y)) by A9, A11, MATRIXC1:1;
then A14: j <= len M by A1, A2, Def4;
A15: 1 <= i by A11, MATRIXC1:1;
A16: i <= width (QuadraticForm (x,M,y)) by A7, A11, MATRIXC1:1;
then  i <= width M by A1, A2, Def4;
then A17: [j,i] in Indices M by A12, A15, A14, MATRIXC1:1;
A18: j <= width (M @) by A1, A2, A5, A13, Def4;
A19: 1 <= i by A11, MATRIXC1:1;
 1 <= i by A11, MATRIXC1:1;
then A20: [j,i] in Indices (QuadraticForm (x,M,y)) by A16, A12, A13, MATRIXC1:1;
 i <= len (M @) by A1, A2, A4, A16, Def4;
then  [i,j] in Indices (M @) by A12, A19, A18, MATRIXC1:1;
then (QuadraticForm (y,(M @),x)) * (i,j) = ((y . i) * ((M @) * (i,j))) * (x . j) by A4, A5, Def4
.= ((y . i) * (M * (j,i))) * (x . j) by A17, MATRIX_1:def_6
.= ((x . j) * (M * (j,i))) * (y . i)
.= (QuadraticForm (x,M,y)) * (j,i) by A1, A2, A17, Def4
.= ((QuadraticForm (x,M,y)) @) * (i,j) by A20, MATRIX_1:def_6 ;
hence  (QuadraticForm (y,(M @),x)) * (i,j) = ((QuadraticForm (x,M,y)) @) * (i,j) ; ::_thesis: verum
end;
A21: len ((QuadraticForm (x,M,y)) @) = width (QuadraticForm (x,M,y)) by MATRIX_1:def_6
.= len y by A1, A2, Def4 ;
width ((QuadraticForm (x,M,y)) @) = len (QuadraticForm (x,M,y)) by A3, A8, MATRIX_2:10
.= len x by A1, A2, Def4 ;
hence  (QuadraticForm (x,M,y)) @ = QuadraticForm (y,(M @),x) by A21, A6, A10, MATRIX_1:21; ::_thesis: verum
end;

theorem Th44: :: MATRPROB:44
for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
|(x,(M * y))| = SumAll (QuadraticForm (x,M,y))
proof
let x, y be FinSequence of REAL ; ::_thesis: for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
|(x,(M * y))| = SumAll (QuadraticForm (x,M,y))
let M be Matrix of REAL; ::_thesis: ( len x = len M & len y = width M & len y > 0 implies |(x,(M * y))| = SumAll (QuadraticForm (x,M,y)) )
set Z = QuadraticForm (x,M,y);
assume that
A1: len x = len M and
A2: len y = width M and
A3: len y > 0 ; ::_thesis: |(x,(M * y))| = SumAll (QuadraticForm (x,M,y))
A4: width (QuadraticForm (x,M,y)) = len y by A1, A2, Def4;
A5: len (LineSum (QuadraticForm (x,M,y))) = len (QuadraticForm (x,M,y)) by Th20;
 len (M * y) = len x by A1, A2, A3, MATRIXR1:61;
then A6: len (mlt (x,(M * y))) = len x by Th30
.= len (LineSum (QuadraticForm (x,M,y))) by A1, A2, A5, Def4 ;
 for i being Nat st 1 <= i & i <= len (LineSum (QuadraticForm (x,M,y))) holds
(LineSum (QuadraticForm (x,M,y))) . i = (mlt (x,(M * y))) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (LineSum (QuadraticForm (x,M,y))) implies (LineSum (QuadraticForm (x,M,y))) . i = (mlt (x,(M * y))) . i )
assume that
A7: 1 <= i and
A8: i <= len (LineSum (QuadraticForm (x,M,y))) ; ::_thesis: (LineSum (QuadraticForm (x,M,y))) . i = (mlt (x,(M * y))) . i
A9: i in Seg (len (LineSum (QuadraticForm (x,M,y)))) by A7, A8, FINSEQ_1:1;
then A10: i in Seg (len M) by A1, A2, A5, Def4;
then A11: i in Seg (len (M * y)) by A2, A3, MATRIXR1:61;
A12: len (Line (M,i)) = len y by A2, MATRIX_1:def_7;
A13: i <= len M by A10, FINSEQ_1:1;
A14: for j being Nat st 1 <= j & j <= len (Line ((QuadraticForm (x,M,y)),i)) holds
((x . i) * (mlt ((Line (M,i)),y))) . j = (Line ((QuadraticForm (x,M,y)),i)) . j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= len (Line ((QuadraticForm (x,M,y)),i)) implies ((x . i) * (mlt ((Line (M,i)),y))) . j = (Line ((QuadraticForm (x,M,y)),i)) . j )
assume that
A15: 1 <= j and
A16: j <= len (Line ((QuadraticForm (x,M,y)),i)) ; ::_thesis: ((x . i) * (mlt ((Line (M,i)),y))) . j = (Line ((QuadraticForm (x,M,y)),i)) . j
 j <= width M by A2, A4, A16, MATRIX_1:def_7;
then A17: [i,j] in Indices M by A7, A13, A15, MATRIXC1:1;
 j in Seg (len (Line ((QuadraticForm (x,M,y)),i))) by A15, A16, FINSEQ_1:1;
then A18: j in Seg (width (QuadraticForm (x,M,y))) by MATRIX_1:def_7;
thus ((x . i) * (mlt ((Line (M,i)),y))) . j = (x . i) * ((mlt ((Line (M,i)),y)) . j) by RVSUM_1:44
.= (x . i) * (((Line (M,i)) . j) * (y . j)) by RVSUM_1:59
.= (x . i) * ((M * (i,j)) * (y . j)) by A2, A4, A18, MATRIX_1:def_7
.= ((x . i) * (M * (i,j))) * (y . j)
.= (QuadraticForm (x,M,y)) * (i,j) by A1, A2, A17, Def4
.= (Line ((QuadraticForm (x,M,y)),i)) . j by A18, MATRIX_1:def_7 ; ::_thesis: verum
end;
A19: len (Line ((QuadraticForm (x,M,y)),i)) = len y by A4, MATRIX_1:def_7;
 len (mlt ((Line (M,i)),y)) = len y by A12, Th30;
then  len ((x . i) * (mlt ((Line (M,i)),y))) = len (Line ((QuadraticForm (x,M,y)),i)) by A19, RVSUM_1:117;
then A20: (x . i) * (mlt ((Line (M,i)),y)) = Line ((QuadraticForm (x,M,y)),i) by A14, FINSEQ_1:14;
(mlt (x,(M * y))) . i = (x . i) * ((M * y) . i) by RVSUM_1:59
.= (x . i) * ((Line (M,i)) "*" y) by A2, A3, A11, Th41
.= Sum ((x . i) * (mlt ((Line (M,i)),y))) by RVSUM_1:87 ;
hence  (LineSum (QuadraticForm (x,M,y))) . i = (mlt (x,(M * y))) . i by A5, A9, A20, Th20; ::_thesis: verum
end;
hence  |(x,(M * y))| = SumAll (QuadraticForm (x,M,y)) by A6, FINSEQ_1:14; ::_thesis: verum
end;

theorem :: MATRPROB:45
for x being FinSequence of REAL holds |(x,((len x) |-> 1))| = Sum x by Th32;

theorem Th46: :: MATRPROB:46
for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M & len y = width M holds
|((x * M),y)| = SumAll (QuadraticForm (x,M,y))
proof
let x, y be FinSequence of REAL ; ::_thesis: for M being Matrix of REAL st len x = len M & len y = width M holds
|((x * M),y)| = SumAll (QuadraticForm (x,M,y))
let M be Matrix of REAL; ::_thesis: ( len x = len M & len y = width M implies |((x * M),y)| = SumAll (QuadraticForm (x,M,y)) )
set Z = QuadraticForm (x,M,y);
assume that
A1: len x = len M and
A2: len y = width M ; ::_thesis: |((x * M),y)| = SumAll (QuadraticForm (x,M,y))
A3: len (QuadraticForm (x,M,y)) = len x by A1, A2, Def4;
A4: len (ColSum (QuadraticForm (x,M,y))) = width (QuadraticForm (x,M,y)) by Def2;
 len (x * M) = len y by A1, A2, MATRIXR1:62;
then A5: len (mlt ((x * M),y)) = len y by Th30
.= len (ColSum (QuadraticForm (x,M,y))) by A1, A2, A4, Def4 ;
 for i being Nat st 1 <= i & i <= len (ColSum (QuadraticForm (x,M,y))) holds
(ColSum (QuadraticForm (x,M,y))) . i = (mlt ((x * M),y)) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (ColSum (QuadraticForm (x,M,y))) implies (ColSum (QuadraticForm (x,M,y))) . i = (mlt ((x * M),y)) . i )
assume that
A6: 1 <= i and
A7: i <= len (ColSum (QuadraticForm (x,M,y))) ; ::_thesis: (ColSum (QuadraticForm (x,M,y))) . i = (mlt ((x * M),y)) . i
A8: i in Seg (len (ColSum (QuadraticForm (x,M,y)))) by A6, A7, FINSEQ_1:1;
then A9: i in Seg (width M) by A1, A2, A4, Def4;
then A10: i in Seg (len (x * M)) by A1, MATRIXR1:62;
A11: len (Col (M,i)) = len x by A1, MATRIX_1:def_8;
A12: i <= width M by A9, FINSEQ_1:1;
A13: for j being Nat st 1 <= j & j <= len (Col ((QuadraticForm (x,M,y)),i)) holds
((y . i) * (mlt (x,(Col (M,i))))) . j = (Col ((QuadraticForm (x,M,y)),i)) . j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= len (Col ((QuadraticForm (x,M,y)),i)) implies ((y . i) * (mlt (x,(Col (M,i))))) . j = (Col ((QuadraticForm (x,M,y)),i)) . j )
assume that
A14: 1 <= j and
A15: j <= len (Col ((QuadraticForm (x,M,y)),i)) ; ::_thesis: ((y . i) * (mlt (x,(Col (M,i))))) . j = (Col ((QuadraticForm (x,M,y)),i)) . j
 j <= len M by A1, A3, A15, MATRIX_1:def_8;
then A16: [j,i] in Indices M by A6, A12, A14, MATRIXC1:1;
 j in Seg (len (Col ((QuadraticForm (x,M,y)),i))) by A14, A15, FINSEQ_1:1;
then A17: j in Seg (len (QuadraticForm (x,M,y))) by MATRIX_1:def_8;
then A18: j in dom (QuadraticForm (x,M,y)) by FINSEQ_1:def_3;
A19: j in dom M by A1, A3, A17, FINSEQ_1:def_3;
thus ((y . i) * (mlt (x,(Col (M,i))))) . j = (y . i) * ((mlt (x,(Col (M,i)))) . j) by RVSUM_1:44
.= (y . i) * ((x . j) * ((Col (M,i)) . j)) by RVSUM_1:59
.= (y . i) * ((x . j) * (M * (j,i))) by A19, MATRIX_1:def_8
.= (QuadraticForm (x,M,y)) * (j,i) by A1, A2, A16, Def4
.= (Col ((QuadraticForm (x,M,y)),i)) . j by A18, MATRIX_1:def_8 ; ::_thesis: verum
end;
A20: len (Col ((QuadraticForm (x,M,y)),i)) = len x by A3, MATRIX_1:def_8;
 len (mlt (x,(Col (M,i)))) = len x by A11, Th30;
then  len ((y . i) * (mlt (x,(Col (M,i))))) = len (Col ((QuadraticForm (x,M,y)),i)) by A20, RVSUM_1:117;
then A21: (y . i) * (mlt (x,(Col (M,i)))) = Col ((QuadraticForm (x,M,y)),i) by A13, FINSEQ_1:14;
(mlt ((x * M),y)) . i = ((x * M) . i) * (y . i) by RVSUM_1:59
.= (x "*" (Col (M,i))) * (y . i) by A1, A10, Th40
.= Sum ((y . i) * (mlt (x,(Col (M,i))))) by RVSUM_1:87 ;
hence  (ColSum (QuadraticForm (x,M,y))) . i = (mlt ((x * M),y)) . i by A4, A8, A21, Def2; ::_thesis: verum
end;
hence |((x * M),y)| = Sum (ColSum (QuadraticForm (x,M,y))) by A5, FINSEQ_1:14
.= SumAll (QuadraticForm (x,M,y)) by Th29 ;
::_thesis: verum
end;

theorem Th47: :: MATRPROB:47
for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
|((x * M),y)| = |(x,(M * y))|
proof
let x, y be FinSequence of REAL ; ::_thesis: for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
|((x * M),y)| = |(x,(M * y))|
let M be Matrix of REAL; ::_thesis: ( len x = len M & len y = width M & len y > 0 implies |((x * M),y)| = |(x,(M * y))| )
assume that
A1: ( len x = len M & len y = width M ) and
A2: len y > 0 ; ::_thesis: |((x * M),y)| = |(x,(M * y))|
thus |((x * M),y)| = SumAll (QuadraticForm (x,M,y)) by A1, Th46
.= |(x,(M * y))| by A1, A2, Th44 ; ::_thesis: verum
end;

theorem :: MATRPROB:48
for x, y being FinSequence of REAL
for M being Matrix of REAL st len y = len M & len x = width M & len x > 0 & len y > 0 holds
|((M * x),y)| = |(x,((M @) * y))|
proof
let x, y be FinSequence of REAL ; ::_thesis: for M being Matrix of REAL st len y = len M & len x = width M & len x > 0 & len y > 0 holds
|((M * x),y)| = |(x,((M @) * y))|
let M be Matrix of REAL; ::_thesis: ( len y = len M & len x = width M & len x > 0 & len y > 0 implies |((M * x),y)| = |(x,((M @) * y))| )
assume that
A1: len y = len M and
A2: len x = width M and
A3: len x > 0 and
A4: len y > 0 ; ::_thesis: |((M * x),y)| = |(x,((M @) * y))|
A5: ( len (M @) = width M & width (M @) = len M ) by A2, A3, MATRIX_2:10;
thus |((M * x),y)| = |((x * (M @)),y)| by A1, A2, A3, A4, MATRIXR1:53
.= |(x,((M @) * y))| by A1, A2, A4, A5, Th47 ; ::_thesis: verum
end;

theorem Th49: :: MATRPROB:49
for x, y being FinSequence of REAL
for M being Matrix of REAL st len y = len M & len x = width M & len x > 0 & len y > 0 holds
|(x,(y * M))| = |((x * (M @)),y)|
proof
let x, y be FinSequence of REAL ; ::_thesis: for M being Matrix of REAL st len y = len M & len x = width M & len x > 0 & len y > 0 holds
|(x,(y * M))| = |((x * (M @)),y)|
let M be Matrix of REAL; ::_thesis: ( len y = len M & len x = width M & len x > 0 & len y > 0 implies |(x,(y * M))| = |((x * (M @)),y)| )
assume that
A1: len y = len M and
A2: len x = width M and
A3: len x > 0 and
A4: len y > 0 ; ::_thesis: |(x,(y * M))| = |((x * (M @)),y)|
A5: ( len (M @) = width M & width (M @) = len M ) by A2, A3, MATRIX_2:10;
thus |(x,(y * M))| = |(x,((M @) * y))| by A1, A2, A3, A4, MATRIXR1:52
.= |((x * (M @)),y)| by A1, A2, A4, A5, Th47 ; ::_thesis: verum
end;

theorem Th50: :: MATRPROB:50
for x being FinSequence of REAL
for M being Matrix of REAL st len x = len M & x = (len x) |-> 1 holds
for k being Element of NAT st k in Seg (len (x * M)) holds
(x * M) . k = Sum (Col (M,k))
proof
let x be FinSequence of REAL ; ::_thesis: for M being Matrix of REAL st len x = len M & x = (len x) |-> 1 holds
for k being Element of NAT st k in Seg (len (x * M)) holds
(x * M) . k = Sum (Col (M,k))
let M be Matrix of REAL; ::_thesis: ( len x = len M & x = (len x) |-> 1 implies for k being Element of NAT st k in Seg (len (x * M)) holds
(x * M) . k = Sum (Col (M,k)) )
assume that
A1: len x = len M and
A2: x = (len x) |-> 1 ; ::_thesis: for k being Element of NAT st k in Seg (len (x * M)) holds
(x * M) . k = Sum (Col (M,k))
hereby  ::_thesis: verum
let k be Element of NAT ; ::_thesis: ( k in Seg (len (x * M)) implies (x * M) . k = Sum (Col (M,k)) )
assume A3: k in Seg (len (x * M)) ; ::_thesis: (x * M) . k = Sum (Col (M,k))
A4: len (Col (M,k)) = len x by A1, MATRIX_1:def_8;
thus (x * M) . k = x "*" (Col (M,k)) by A1, A3, Th40
.= Sum (Col (M,k)) by A2, A4, Th32 ; ::_thesis: verum
end;
end;

theorem :: MATRPROB:51
for x being FinSequence of REAL
for M being Matrix of REAL st len x = width M & width M > 0 & x = (len x) |-> 1 holds
for k being Element of NAT st k in Seg (len (M * x)) holds
(M * x) . k = Sum (Line (M,k))
proof
let x be FinSequence of REAL ; ::_thesis: for M being Matrix of REAL st len x = width M & width M > 0 & x = (len x) |-> 1 holds
for k being Element of NAT st k in Seg (len (M * x)) holds
(M * x) . k = Sum (Line (M,k))
let M be Matrix of REAL; ::_thesis: ( len x = width M & width M > 0 & x = (len x) |-> 1 implies for k being Element of NAT st k in Seg (len (M * x)) holds
(M * x) . k = Sum (Line (M,k)) )
assume that
A1: len x = width M and
A2: width M > 0 and
A3: x = (len x) |-> 1 ; ::_thesis: for k being Element of NAT st k in Seg (len (M * x)) holds
(M * x) . k = Sum (Line (M,k))
hereby  ::_thesis: verum
let k be Element of NAT ; ::_thesis: ( k in Seg (len (M * x)) implies (M * x) . k = Sum (Line (M,k)) )
assume A4: k in Seg (len (M * x)) ; ::_thesis: (M * x) . k = Sum (Line (M,k))
A5: len (Line (M,k)) = len x by A1, MATRIX_1:def_7;
thus (M * x) . k = (Line (M,k)) "*" x by A1, A2, A4, Th41
.= Sum (Line (M,k)) by A3, A5, Th32 ; ::_thesis: verum
end;
end;

theorem Th52: :: MATRPROB:52
for n being non empty Nat ex P being FinSequence of REAL st
( len P = n & ( for i being Element of NAT st i in dom P holds
P . i >= 0 ) & Sum P = 1 )
proof
let n be non empty Nat; ::_thesis: ex P being FinSequence of REAL st
( len P = n & ( for i being Element of NAT st i in dom P holds
P . i >= 0 ) & Sum P = 1 )
reconsider n = n as non empty Element of NAT by ORDINAL1:def_12;
consider e being FinSequence of REAL  such that
A1: len e = n and
A2: for i being Nat st i in Seg n holds
( ( i in Seg 1 implies e . i = 1 ) & ( not i in Seg 1 implies e . i = 0 ) ) by Th2;
A3: n >= 1 by NAT_1:14;
A4: Sum e = 1
proof
consider f being Real_Sequence such that
A5: f . 1 = e . 1 and
A6: for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) and
A7: Sum e = f . (len e) by A1, NAT_1:14, PROB_3:63;
 for n being Nat st n <> 0 & n <= len e holds
f . n = 1
proof
defpred S1[ Nat] means ( $1 <> 0 & $1 <= len e implies f . $1 = 1 );
A8: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_(_k_+_1_<>_0_&_k_+_1_<=_len_e_implies_f_._(k_+_1)_=_1_)
assume that
 k + 1 <> 0 and
A10: k + 1 <= len e ; ::_thesis: f . (k + 1) = 1
percases ( ( k = 0 & k < len e ) or ( k > 0 & k < len e ) ) by A10, NAT_1:13;
supposeA11: ( k = 0 & k < len e ) ; ::_thesis: f . (k + 1) = 1
 ( 1 in Seg 1 & 1 in Seg n ) by A3, FINSEQ_1:1;
hence  f . (k + 1) = 1 by A2, A5, A11; ::_thesis: verum
end;
supposeA12: ( k > 0 & k < len e ) ; ::_thesis: f . (k + 1) = 1
then  k >= 1 by NAT_1:14;
then  k + 1 > 1 by NAT_1:13;
then A13: ( k + 1 in Seg n & not k + 1 in Seg 1 ) by A1, A10, FINSEQ_1:1;
thus f . (k + 1) = 1 + (e . (k + 1)) by A6, A9, A12
.= 1 + 0 by A2, A13
.= 1 ; ::_thesis: verum
end;
end;
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A14: S1[ 0 ] ;
 for n being Nat holds S1[n] from NAT_1:sch_2(A14, A8);
hence  for n being Nat st n <> 0 & n <= len e holds
f . n = 1 ; ::_thesis: verum
end;
hence  Sum e = 1 by A1, A7; ::_thesis: verum
end;
take  e ; ::_thesis: ( len e = n & ( for i being Element of NAT st i in dom e holds
e . i >= 0 ) & Sum e = 1 )
 for i being Element of NAT st i in dom e holds
e . i >= 0
proof
let i be Element of NAT ; ::_thesis: ( i in dom e implies e . i >= 0 )
assume  i in dom e ; ::_thesis: e . i >= 0
then  i in Seg n by A1, FINSEQ_1:def_3;
hence  e . i >= 0 by A2; ::_thesis: verum
end;
hence  ( len e = n & ( for i being Element of NAT st i in dom e holds
e . i >= 0 ) & Sum e = 1 ) by A1, A4; ::_thesis: verum
end;

definition
let p be FinSequence of REAL ;
attrp is ProbFinS  means :Def5: :: MATRPROB:def 5
( ( for i being Element of NAT st i in dom p holds
p . i >= 0 ) & Sum p = 1 );
end;

:: deftheorem Def5 defines ProbFinS MATRPROB:def_5_:_
 for p being FinSequence of REAL holds
( p is ProbFinS iff ( ( for i being Element of NAT st i in dom p holds
p . i >= 0 ) & Sum p = 1 ) );

registration
cluster non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() ProbFinS for FinSequence of REAL ;
existence
 ex b1 being FinSequence of REAL st
( not b1 is empty & b1 is ProbFinS )
proof
set n = 1;
consider p being FinSequence of REAL  such that
A1: ( len p = 1 & ( for i being Element of NAT st i in dom p holds
p . i >= 0 ) & Sum p = 1 ) by Th52;
take  p ; ::_thesis: ( not p is empty & p is ProbFinS )
thus  ( not p is empty & p is ProbFinS ) by A1, Def5; ::_thesis: verum
end;
end;

theorem :: MATRPROB:53
for p being non empty ProbFinS FinSequence of REAL
for k being Element of NAT st k in dom p holds
p . k <= 1
proof
let p be non empty ProbFinS FinSequence of REAL ; ::_thesis: for k being Element of NAT st k in dom p holds
p . k <= 1
 ( Sum p = 1 & ( for i being Nat st i in dom p holds
p . i >= 0 ) ) by Def5;
hence  for k being Element of NAT st k in dom p holds
p . k <= 1 by Th5; ::_thesis: verum
end;

theorem Th54: :: MATRPROB:54
for D being non empty set
for M being non empty-yielding Matrix of D holds
( 1 <= len M & 1 <= width M )
proof
let D be non empty set ; ::_thesis: for M being non empty-yielding Matrix of D holds
( 1 <= len M & 1 <= width M )
let M be non empty-yielding Matrix of D; ::_thesis: ( 1 <= len M & 1 <= width M )
 ( not len M = 0 & not width M = 0 ) by GOBOARD1:def_3;
hence  ( 1 <= len M & 1 <= width M ) by NAT_1:14; ::_thesis: verum
end;

definition
let M be Matrix of REAL;
attrM is m-nonnegative  means :Def6: :: MATRPROB:def 6
 for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) >= 0 ;
end;

:: deftheorem Def6 defines m-nonnegative MATRPROB:def_6_:_
 for M being Matrix of REAL holds
( M is m-nonnegative iff for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) >= 0 );

definition
let M be Matrix of REAL;
attrM is with_sum=1  means :Def7: :: MATRPROB:def 7
 SumAll M = 1;
end;

:: deftheorem Def7 defines with_sum=1 MATRPROB:def_7_:_
 for M being Matrix of REAL holds
( M is with_sum=1 iff SumAll M = 1 );

definition
let M be Matrix of REAL;
attrM is Joint_Probability  means :Def8: :: MATRPROB:def 8
( M is m-nonnegative & M is with_sum=1 );
end;

:: deftheorem Def8 defines Joint_Probability MATRPROB:def_8_:_
 for M being Matrix of REAL holds
( M is Joint_Probability iff ( M is m-nonnegative & M is with_sum=1 ) );

registration
cluster tabular Joint_Probability  ->  m-nonnegative with_sum=1 for FinSequence of REAL * ;
coherence
 for b1 being Matrix of REAL st b1 is Joint_Probability holds
( b1 is m-nonnegative & b1 is with_sum=1 ) by Def8;
cluster tabular m-nonnegative with_sum=1  ->  Joint_Probability for FinSequence of REAL * ;
coherence
 for b1 being Matrix of REAL st b1 is m-nonnegative & b1 is with_sum=1 holds
b1 is Joint_Probability by Def8;
end;

theorem Th55: :: MATRPROB:55
for n, m being non empty Nat ex M being Matrix of n,m, REAL st
( M is m-nonnegative & SumAll M = 1 )
proof
let n, m be non empty Nat; ::_thesis: ex M being Matrix of n,m, REAL st
( M is m-nonnegative & SumAll M = 1 )
consider m1 being Nat such that
A1: m = m1 + 1 by NAT_1:6;
consider n1 being Nat such that
A2: n = n1 + 1 by NAT_1:6;
reconsider n = n, m = m as non empty Element of NAT by ORDINAL1:def_12;
reconsider m1 = m1, n1 = n1 as Element of NAT by ORDINAL1:def_12;
consider e1 being FinSequence of REAL  such that
A3: len e1 = m and
A4: for i being Nat st i in Seg m holds
( ( i in Seg m1 implies e1 . i = 0 ) & ( not i in Seg m1 implies e1 . i = 1 ) ) by Th2;
 m1 + 1 > m1 by NAT_1:13;
then A5: not m1 + 1 in Seg m1 by FINSEQ_1:1;
 m1 + 1 in Seg m by A1, FINSEQ_1:4;
then  e1 . (m1 + 1) = 1 by A4, A5;
then A6: e1 = (e1 | m1) ^ <*1*> by A1, A3, RFINSEQ:7;
reconsider e3 = e1 | m1 as FinSequence of REAL ;
 m > m1 by A1, NAT_1:13;
then A7: len e3 = m1 by A3, FINSEQ_1:59;
A8: dom e1 = Seg m by A3, FINSEQ_1:def_3;
A9: Sum e1 = 1
proof
percases ( m1 = 0 or m1 <> 0 ) ;
suppose m1 = 0 ; ::_thesis: Sum e1 = 1
then A10: Sum e3 = 0 by RVSUM_1:72;
thus  Sum e1 = (Sum (e1 | m1)) + 1 by A6, RVSUM_1:74
.= 1 by A10 ; ::_thesis: verum
end;
supposeA11: m1 <> 0 ; ::_thesis: Sum e1 = 1
 for i being Nat st i in dom e3 holds
e3 . i = 0
proof
let i be Nat; ::_thesis: ( i in dom e3 implies e3 . i = 0 )
assume  i in dom e3 ; ::_thesis: e3 . i = 0
then A12: i in Seg m1 by A7, FINSEQ_1:def_3;
 m1 + 1 in Seg (m1 + 1) by FINSEQ_1:4;
then  m1 in Seg m by A1, A11, FINSEQ_1:61;
then  m1 in dom e1 by A3, FINSEQ_1:def_3;
then  ( e3 . i = e1 . i & i in dom e1 ) by A12, RFINSEQ:6;
hence  e3 . i = 0 by A4, A8, A12; ::_thesis: verum
end;
then  e3 = m1 |-> 0 by A7, A11, Th1;
then A13: Sum e3 = m1 * 0 by RVSUM_1:80
.= 0 ;
thus  Sum e1 = (Sum (e1 | m1)) + 1 by A6, RVSUM_1:74
.= 1 by A13 ; ::_thesis: verum
end;
end;
end;
reconsider e2 = m |-> 0 as FinSequence of REAL ;
 len e2 = m by CARD_1:def_7;
then consider M1 being Matrix of n,m, REAL  such that
A14: for i being Nat st i in Seg n holds
( ( i in Seg n1 implies M1 . i = e2 ) & ( not i in Seg n1 implies M1 . i = e1 ) ) by A3, Th19;
A15: Sum e2 = m * 0 by RVSUM_1:80
.= 0 ;
A16: ( len (Sum M1) = n & ( for i being Element of NAT st i in Seg n holds
( ( i in Seg n1 implies (Sum M1) . i = 0 ) & ( not i in Seg n1 implies (Sum M1) . i = 1 ) ) ) )
proof
thus A17: len (Sum M1) = len M1 by Def1
.= n by MATRIX_1:def_2 ; ::_thesis: for i being Element of NAT st i in Seg n holds
( ( i in Seg n1 implies (Sum M1) . i = 0 ) & ( not i in Seg n1 implies (Sum M1) . i = 1 ) )
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( ( i in Seg n1 implies (Sum M1) . i = 0 ) & ( not i in Seg n1 implies (Sum M1) . i = 1 ) ) )
assume A18: i in Seg n ; ::_thesis: ( ( i in Seg n1 implies (Sum M1) . i = 0 ) & ( not i in Seg n1 implies (Sum M1) . i = 1 ) )
A19: i in dom (Sum M1) by A17, A18, FINSEQ_1:def_3;
thus  ( i in Seg n1 implies (Sum M1) . i = 0 ) ::_thesis: ( not i in Seg n1 implies (Sum M1) . i = 1 )
proof
assume A20: i in Seg n1 ; ::_thesis: (Sum M1) . i = 0
thus (Sum M1) . i = Sum (M1 . i) by A19, Def1
.= 0 by A14, A15, A18, A20 ; ::_thesis: verum
end;
assume A21: not i in Seg n1 ; ::_thesis: (Sum M1) . i = 1
thus (Sum M1) . i = Sum (M1 . i) by A19, Def1
.= 1 by A14, A9, A18, A21 ; ::_thesis: verum
end;
A22: SumAll M1 = 1
proof
reconsider e4 = Sum M1 as FinSequence of REAL ;
reconsider e5 = e4 | n1 as FinSequence of REAL ;
 n1 + 1 > n1 by NAT_1:13;
then A23: not n1 + 1 in Seg n1 by FINSEQ_1:1;
 n1 + 1 in Seg n by A2, FINSEQ_1:4;
then A24: e4 . (n1 + 1) = 1 by A16, A23;
 n > n1 by A2, NAT_1:13;
then A25: len e5 = n1 by A16, FINSEQ_1:59;
A26: dom e4 = Seg n by A16, FINSEQ_1:def_3;
 Sum e4 = 1
proof
percases ( n1 = 0 or n1 <> 0 ) ;
suppose n1 = 0 ; ::_thesis: Sum e4 = 1
then A27: e5 = <*> REAL ;
thus  Sum e4 = Sum ((e4 | n1) ^ <*1*>) by A2, A16, A24, RFINSEQ:7
.= (Sum (e4 | n1)) + 1 by RVSUM_1:74
.= 1 by A27, RVSUM_1:72 ; ::_thesis: verum
end;
supposeA28: n1 <> 0 ; ::_thesis: Sum e4 = 1
 for i being Nat st i in dom e5 holds
e5 . i = 0
proof
let i be Nat; ::_thesis: ( i in dom e5 implies e5 . i = 0 )
assume  i in dom e5 ; ::_thesis: e5 . i = 0
then A29: i in Seg n1 by A25, FINSEQ_1:def_3;
 n1 + 1 in Seg (n1 + 1) by FINSEQ_1:4;
then  n1 in Seg n by A2, A28, FINSEQ_1:61;
then  n1 in dom e4 by A16, FINSEQ_1:def_3;
then  ( e5 . i = e4 . i & i in dom e4 ) by A29, RFINSEQ:6;
hence  e5 . i = 0 by A16, A26, A29; ::_thesis: verum
end;
then  e5 = n1 |-> 0 by A25, A28, Th1;
then A30: Sum e5 = n1 * 0 by RVSUM_1:80
.= 0 ;
thus  Sum e4 = Sum ((e4 | n1) ^ <*1*>) by A2, A16, A24, RFINSEQ:7
.= (Sum (e4 | n1)) + 1 by RVSUM_1:74
.= 1 by A30 ; ::_thesis: verum
end;
end;
end;
hence  SumAll M1 = 1 ; ::_thesis: verum
end;
 for i, j being Element of NAT st [i,j] in Indices M1 holds
M1 * (i,j) >= 0
proof
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) >= 0 )
assume A31: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) >= 0
consider p1 being FinSequence of REAL  such that
A32: p1 = M1 . i and
A33: M1 * (i,j) = p1 . j by A31, MATRIX_1:def_5;
A34: len M1 = n by MATRIX_1:def_2;
A35: [i,j] in [:(dom M1),(Seg (width M1)):] by A31, MATRIX_1:def_4;
then  i in dom M1 by ZFMISC_1:87;
then A36: i in Seg n by A34, FINSEQ_1:def_3;
 j in Seg (width M1) by A35, ZFMISC_1:87;
then A37: j in Seg m by A34, MATRIX_1:20;
percases ( p1 = e2 or p1 = e1 ) by A14, A32, A36;
suppose p1 = e2 ; ::_thesis: M1 * (i,j) >= 0
hence  M1 * (i,j) >= 0 by A33; ::_thesis: verum
end;
suppose p1 = e1 ; ::_thesis: M1 * (i,j) >= 0
hence  M1 * (i,j) >= 0 by A4, A33, A37; ::_thesis: verum
end;
end;
end;
then  M1 is m-nonnegative by Def6;
hence  ex M being Matrix of n,m, REAL st
( M is m-nonnegative & SumAll M = 1 ) by A22; ::_thesis: verum
end;

registration
cluster Relation-like non empty-yielding NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() Joint_Probability for FinSequence of REAL * ;
existence
 ex b1 being Matrix of REAL st
( not b1 is empty-yielding & b1 is Joint_Probability )
proof
set n = 1;
set m = 1;
consider M being Matrix of 1,1, REAL  such that
A1: M is m-nonnegative and
A2: SumAll M = 1 by Th55;
take  M ; ::_thesis: ( not M is empty-yielding & M is Joint_Probability )
A3: M is with_sum=1 by A2, Def7;
A4: len M = 1 by MATRIX_1:def_2;
then  width M = 1 by MATRIX_1:20;
hence  ( not M is empty-yielding & M is Joint_Probability ) by A1, A4, A3, GOBOARD1:def_3; ::_thesis: verum
end;
end;

theorem Th56: :: MATRPROB:56
for M being non empty-yielding Joint_Probability Matrix of REAL holds M @ is non empty-yielding Joint_Probability Matrix of REAL
proof
let M be non empty-yielding Joint_Probability Matrix of REAL; ::_thesis: M @ is non empty-yielding Joint_Probability Matrix of REAL
set n = len M;
set m = width M;
A1: len M > 0 by Th54;
A2: width M > 0 by Th54;
then A3: ( len (M @) = width M & width (M @) = len M ) by MATRIX_2:10;
then reconsider M1 = M @ as Matrix of width M, len M, REAL by MATRIX_2:7;
 for i, j being Element of NAT st [i,j] in Indices M1 holds
M1 * (i,j) >= 0
proof
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) >= 0 )
assume  [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) >= 0
then A4: [j,i] in Indices M by MATRIX_1:def_6;
then  M1 * (i,j) = M * (j,i) by MATRIX_1:def_6;
hence  M1 * (i,j) >= 0 by A4, Def6; ::_thesis: verum
end;
then A5: M1 is m-nonnegative by Def6;
SumAll M1 = SumAll M by Th28
.= 1 by Def7 ;
then  M1 is with_sum=1 by Def7;
hence  M @ is non empty-yielding Joint_Probability Matrix of REAL by A1, A2, A3, A5, GOBOARD1:def_3; ::_thesis: verum
end;

theorem :: MATRPROB:57
for M being non empty-yielding Joint_Probability Matrix of REAL
for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) <= 1
proof
let M be non empty-yielding Joint_Probability Matrix of REAL; ::_thesis: for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) <= 1
A1: for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) >= 0 by Def6;
A2: for i being Nat st i in dom (Sum M) holds
(Sum M) . i >= 0
proof
let i be Nat; ::_thesis: ( i in dom (Sum M) implies (Sum M) . i >= 0 )
assume A3: i in dom (Sum M) ; ::_thesis: (Sum M) . i >= 0
 i in Seg (len (Sum M)) by A3, FINSEQ_1:def_3;
then  i in Seg (len M) by Def1;
then  i in dom M by FINSEQ_1:def_3;
then  for j being Nat st j in dom (M . i) holds
(M . i) . j >= 0 by A1, Lm1;
then  Sum (M . i) >= 0 by RVSUM_1:84;
hence  (Sum M) . i >= 0 by A3, Def1; ::_thesis: verum
end;
A4: for i being Element of NAT st i in dom (Sum M) holds
(Sum M) . i <= 1
proof
let i be Element of NAT ; ::_thesis: ( i in dom (Sum M) implies (Sum M) . i <= 1 )
assume  i in dom (Sum M) ; ::_thesis: (Sum M) . i <= 1
then  (Sum M) . i <= SumAll M by A2, Th5;
hence  (Sum M) . i <= 1 by Def7; ::_thesis: verum
end;
A5: for i being Element of NAT st i in dom M holds
for j being Element of NAT st j in dom (M . i) holds
(M . i) . j <= Sum (M . i)
proof
let i be Element of NAT ; ::_thesis: ( i in dom M implies for j being Element of NAT st j in dom (M . i) holds
(M . i) . j <= Sum (M . i) )
assume  i in dom M ; ::_thesis: for j being Element of NAT st j in dom (M . i) holds
(M . i) . j <= Sum (M . i)
then  for j being Nat st j in dom (M . i) holds
(M . i) . j >= 0 by A1, Lm1;
hence  for j being Element of NAT st j in dom (M . i) holds
(M . i) . j <= Sum (M . i) by Th5; ::_thesis: verum
end;
A6: for i being Element of NAT st i in dom M holds
for j being Element of NAT st j in dom (M . i) holds
(M . i) . j <= 1
proof
let i be Element of NAT ; ::_thesis: ( i in dom M implies for j being Element of NAT st j in dom (M . i) holds
(M . i) . j <= 1 )
assume A7: i in dom M ; ::_thesis: for j being Element of NAT st j in dom (M . i) holds
(M . i) . j <= 1
 i in Seg (len M) by A7, FINSEQ_1:def_3;
then  i in Seg (len (Sum M)) by Def1;
then A8: i in dom (Sum M) by FINSEQ_1:def_3;
then  (Sum M) . i <= 1 by A4;
then A9: Sum (M . i) <= 1 by A8, Def1;
let j be Element of NAT ; ::_thesis: ( j in dom (M . i) implies (M . i) . j <= 1 )
assume  j in dom (M . i) ; ::_thesis: (M . i) . j <= 1
then  (M . i) . j <= Sum (M . i) by A5, A7;
hence  (M . i) . j <= 1 by A9, XXREAL_0:2; ::_thesis: verum
end;
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices M implies M * (i,j) <= 1 )
assume A10: [i,j] in Indices M ; ::_thesis: M * (i,j) <= 1
A11: ex p1 being FinSequence of REAL st
( p1 = M . i & M * (i,j) = p1 . j ) by A10, MATRIX_1:def_5;
 i in Seg (len M) by A10, Th12;
then A12: i in dom M by FINSEQ_1:def_3;
 j in Seg (width M) by A10, Th12;
then  j in Seg (len (M . i)) by A12, MATRIX_1:42;
then  j in dom (M . i) by FINSEQ_1:def_3;
hence  M * (i,j) <= 1 by A6, A12, A11; ::_thesis: verum
end;

definition
let M be Matrix of REAL;
attrM is with_line_sum=1  means :Def9: :: MATRPROB:def 9
 for k being Element of NAT st k in dom M holds
Sum (M . k) = 1;
end;

:: deftheorem Def9 defines with_line_sum=1 MATRPROB:def_9_:_
 for M being Matrix of REAL holds
( M is with_line_sum=1 iff for k being Element of NAT st k in dom M holds
Sum (M . k) = 1 );

theorem Th58: :: MATRPROB:58
for n, m being non empty Nat ex M being Matrix of n,m, REAL st
( M is m-nonnegative & M is with_line_sum=1 )
proof
let n, m be non empty Nat; ::_thesis: ex M being Matrix of n,m, REAL st
( M is m-nonnegative & M is with_line_sum=1 )
consider m1 being Nat such that
A1: m = m1 + 1 by NAT_1:6;
reconsider m1 = m1 as Element of NAT by ORDINAL1:def_12;
consider e1 being FinSequence of REAL  such that
A2: len e1 = m and
A3: for i being Nat st i in Seg m holds
( ( i in Seg m1 implies e1 . i = 0 ) & ( not i in Seg m1 implies e1 . i = 1 ) ) by Th2;
 m1 + 1 > m1 by NAT_1:13;
then A4: not m1 + 1 in Seg m1 by FINSEQ_1:1;
 m1 + 1 in Seg m by A1, FINSEQ_1:4;
then  e1 . (m1 + 1) = 1 by A3, A4;
then A5: e1 = (e1 | m1) ^ <*1*> by A1, A2, RFINSEQ:7;
reconsider M1 = n |-> e1 as Matrix of n,m, REAL by A2, Th18;
A6: len M1 = n by MATRIX_1:def_2;
A7: for i, j being Element of NAT st [i,j] in Indices M1 holds
M1 * (i,j) >= 0
proof
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) >= 0 )
assume A8: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) >= 0
consider p1 being FinSequence of REAL  such that
A9: p1 = M1 . i and
A10: M1 * (i,j) = p1 . j by A8, MATRIX_1:def_5;
A11: [i,j] in [:(dom M1),(Seg (width M1)):] by A8, MATRIX_1:def_4;
then  j in Seg (width M1) by ZFMISC_1:87;
then A12: j in Seg m by A6, MATRIX_1:20;
 i in dom M1 by A11, ZFMISC_1:87;
then  i in Seg n by A6, FINSEQ_1:def_3;
then  p1 = e1 by A9, FUNCOP_1:7;
hence  M1 * (i,j) >= 0 by A3, A10, A12; ::_thesis: verum
end;
reconsider e3 = e1 | m1 as FinSequence of REAL ;
 m > m1 by A1, NAT_1:13;
then A13: len e3 = m1 by A2, FINSEQ_1:59;
take  M1 ; ::_thesis: ( M1 is m-nonnegative & M1 is with_line_sum=1 )
A14: dom e1 = Seg m by A2, FINSEQ_1:def_3;
A15: Sum e1 = 1
proof
percases ( m1 = 0 or m1 <> 0 ) ;
suppose m1 = 0 ; ::_thesis: Sum e1 = 1
then A16: e3 = <*> REAL ;
thus  Sum e1 = (Sum (e1 | m1)) + 1 by A5, RVSUM_1:74
.= 1 by A16, RVSUM_1:72 ; ::_thesis: verum
end;
supposeA17: m1 <> 0 ; ::_thesis: Sum e1 = 1
 for i being Nat st i in dom e3 holds
e3 . i = 0
proof
let i be Nat; ::_thesis: ( i in dom e3 implies e3 . i = 0 )
assume  i in dom e3 ; ::_thesis: e3 . i = 0
then A18: i in Seg m1 by A13, FINSEQ_1:def_3;
 m1 + 1 in Seg (m1 + 1) by FINSEQ_1:4;
then  m1 in Seg m by A1, A17, FINSEQ_1:61;
then  m1 in dom e1 by A2, FINSEQ_1:def_3;
then  ( e3 . i = e1 . i & i in dom e1 ) by A18, RFINSEQ:6;
hence  e3 . i = 0 by A3, A14, A18; ::_thesis: verum
end;
then  e3 = m1 |-> 0 by A13, A17, Th1;
then A19: Sum e3 = m1 * 0 by RVSUM_1:80
.= 0 ;
thus  Sum e1 = (Sum (e1 | m1)) + 1 by A5, RVSUM_1:74
.= 1 by A19 ; ::_thesis: verum
end;
end;
end;
 for i being Element of NAT st i in dom M1 holds
Sum (M1 . i) = 1
proof
let i be Element of NAT ; ::_thesis: ( i in dom M1 implies Sum (M1 . i) = 1 )
assume  i in dom M1 ; ::_thesis: Sum (M1 . i) = 1
then  i in Seg n by A6, FINSEQ_1:def_3;
hence  Sum (M1 . i) = 1 by A15, FUNCOP_1:7; ::_thesis: verum
end;
hence  ( M1 is m-nonnegative & M1 is with_line_sum=1 ) by A7, Def6, Def9; ::_thesis: verum
end;

definition
let M be Matrix of REAL;
attrM is Conditional_Probability  means :Def10: :: MATRPROB:def 10
( M is m-nonnegative & M is with_line_sum=1 );
end;

:: deftheorem Def10 defines Conditional_Probability MATRPROB:def_10_:_
 for M being Matrix of REAL holds
( M is Conditional_Probability iff ( M is m-nonnegative & M is with_line_sum=1 ) );

registration
cluster tabular Conditional_Probability  ->  m-nonnegative with_line_sum=1 for FinSequence of REAL * ;
coherence
 for b1 being Matrix of REAL st b1 is Conditional_Probability holds
( b1 is m-nonnegative & b1 is with_line_sum=1 ) by Def10;
cluster tabular m-nonnegative with_line_sum=1  ->  Conditional_Probability for FinSequence of REAL * ;
coherence
 for b1 being Matrix of REAL st b1 is m-nonnegative & b1 is with_line_sum=1 holds
b1 is Conditional_Probability by Def10;
end;

registration
cluster Relation-like non empty-yielding NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() Conditional_Probability for FinSequence of REAL * ;
existence
 ex b1 being Matrix of REAL st
( not b1 is empty-yielding & b1 is Conditional_Probability )
proof
set n = 1;
set m = 1;
consider M being Matrix of 1,1, REAL  such that
A1: ( M is m-nonnegative & M is with_line_sum=1 ) by Th58;
take  M ; ::_thesis: ( not M is empty-yielding & M is Conditional_Probability )
A2: len M = 1 by MATRIX_1:def_2;
then  width M = 1 by MATRIX_1:20;
hence  ( not M is empty-yielding & M is Conditional_Probability ) by A1, A2, GOBOARD1:def_3; ::_thesis: verum
end;
end;

theorem :: MATRPROB:59
for M being non empty-yielding Conditional_Probability Matrix of REAL
for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) <= 1
proof
let M be non empty-yielding Conditional_Probability Matrix of REAL; ::_thesis: for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) <= 1
A1: for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) >= 0 by Def6;
A2: for i being Element of NAT st i in dom M holds
for j being Element of NAT st j in dom (M . i) holds
(M . i) . j <= 1
proof
let i be Element of NAT ; ::_thesis: ( i in dom M implies for j being Element of NAT st j in dom (M . i) holds
(M . i) . j <= 1 )
assume A3: i in dom M ; ::_thesis: for j being Element of NAT st j in dom (M . i) holds
(M . i) . j <= 1
A4: for j being Nat st j in dom (M . i) holds
(M . i) . j >= 0 by A1, A3, Lm1;
let j be Element of NAT ; ::_thesis: ( j in dom (M . i) implies (M . i) . j <= 1 )
assume  j in dom (M . i) ; ::_thesis: (M . i) . j <= 1
then  (M . i) . j <= Sum (M . i) by A4, Th5;
hence  (M . i) . j <= 1 by A3, Def9; ::_thesis: verum
end;
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices M implies M * (i,j) <= 1 )
assume A5: [i,j] in Indices M ; ::_thesis: M * (i,j) <= 1
A6: ex p1 being FinSequence of REAL st
( p1 = M . i & M * (i,j) = p1 . j ) by A5, MATRIX_1:def_5;
 i in Seg (len M) by A5, Th12;
then A7: i in dom M by FINSEQ_1:def_3;
 j in Seg (width M) by A5, Th12;
then  j in Seg (len (M . i)) by A7, MATRIX_1:42;
then  j in dom (M . i) by FINSEQ_1:def_3;
hence  M * (i,j) <= 1 by A2, A7, A6; ::_thesis: verum
end;

theorem Th60: :: MATRPROB:60
for M being non empty-yielding Matrix of REAL holds
( M is non empty-yielding Conditional_Probability Matrix of REAL iff for i being Element of NAT st i in dom M holds
Line (M,i) is non empty ProbFinS FinSequence of REAL )
proof
let M be non empty-yielding Matrix of REAL; ::_thesis: ( M is non empty-yielding Conditional_Probability Matrix of REAL iff for i being Element of NAT st i in dom M holds
Line (M,i) is non empty ProbFinS FinSequence of REAL )
hereby  ::_thesis: ( ( for i being Element of NAT st i in dom M holds
Line (M,i) is non empty ProbFinS FinSequence of REAL ) implies M is non empty-yielding Conditional_Probability Matrix of REAL )
assume A1: M is non empty-yielding Conditional_Probability Matrix of REAL ; ::_thesis: for i being Element of NAT st i in dom M holds
Line (M,i) is non empty ProbFinS FinSequence of REAL
hereby  ::_thesis: verum
set m = width M;
let i be Element of NAT ; ::_thesis: ( i in dom M implies Line (M,i) is non empty ProbFinS FinSequence of REAL )
assume A2: i in dom M ; ::_thesis: Line (M,i) is non empty ProbFinS FinSequence of REAL
 for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) >= 0 by A1, Def6;
then A3: ( len (Line (M,i)) = width M & ( for j being Element of NAT st j in dom (Line (M,i)) holds
(Line (M,i)) . j >= 0 ) ) by A2, Lm2, MATRIX_1:def_7;
Sum (Line (M,i)) = Sum (M . i) by A2, MATRIX_2:16
.= 1 by A1, A2, Def9 ;
hence  Line (M,i) is non empty ProbFinS FinSequence of REAL by A3, Def5, Th54; ::_thesis: verum
end;
end;
assume A4: for i being Element of NAT st i in dom M holds
Line (M,i) is non empty ProbFinS FinSequence of REAL ; ::_thesis: M is non empty-yielding Conditional_Probability Matrix of REAL
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_M_holds_
Sum_(M_._k)_=_1
let k be Element of NAT ; ::_thesis: ( k in dom M implies Sum (M . k) = 1 )
assume A5: k in dom M ; ::_thesis: Sum (M . k) = 1
 Line (M,k) is ProbFinS by A4, A5;
then  Sum (Line (M,k)) = 1 by Def5;
hence  Sum (M . k) = 1 by A5, MATRIX_2:16; ::_thesis: verum
end;
then A6: M is with_line_sum=1 by Def9;
 for i, j being Element of NAT st i in dom M & j in dom (Line (M,i)) holds
(Line (M,i)) . j >= 0
proof
let i, j be Element of NAT ; ::_thesis: ( i in dom M & j in dom (Line (M,i)) implies (Line (M,i)) . j >= 0 )
assume that
A7: i in dom M and
A8: j in dom (Line (M,i)) ; ::_thesis: (Line (M,i)) . j >= 0
 Line (M,i) is ProbFinS by A4, A7;
hence  (Line (M,i)) . j >= 0 by A8, Def5; ::_thesis: verum
end;
then  for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) >= 0 by Lm2;
then  M is m-nonnegative by Def6;
hence  M is non empty-yielding Conditional_Probability Matrix of REAL by A6; ::_thesis: verum
end;

theorem :: MATRPROB:61
for M being non empty-yielding with_line_sum=1 Matrix of REAL holds SumAll M = len M
proof
let M be non empty-yielding with_line_sum=1 Matrix of REAL; ::_thesis: SumAll M = len M
set n = len M;
A1: ( len (Sum M) = len M & ( for i being Nat st i in dom (Sum M) holds
(Sum M) . i = 1 ) )
proof
thus  len (Sum M) = len M by Def1; ::_thesis: for i being Nat st i in dom (Sum M) holds
(Sum M) . i = 1
hereby  ::_thesis: verum
let i be Nat; ::_thesis: ( i in dom (Sum M) implies (Sum M) . i = 1 )
assume A2: i in dom (Sum M) ; ::_thesis: (Sum M) . i = 1
then  i in Seg (len (Sum M)) by FINSEQ_1:def_3;
then  i in Seg (len M) by Def1;
then  i in dom M by FINSEQ_1:def_3;
then  Sum (M . i) = 1 by Def9;
hence  (Sum M) . i = 1 by A2, Def1; ::_thesis: verum
end;
end;
 len M > 0 by Th54;
then  Sum M = (len M) |-> 1 by A1, Th1;
hence  SumAll M = (len M) * 1 by RVSUM_1:80
.= len M ;
::_thesis: verum
end;

notation
let M be Matrix of REAL;
synonym  Row_Marginal M for  LineSum M;
synonym  Column_Marginal M for  ColSum M;
end;

registration
let M be non empty-yielding Joint_Probability Matrix of REAL;
cluster Sum M ->  non empty ProbFinS ;
coherence
 ( not Row_Marginal M is empty & Row_Marginal M is ProbFinS )
proof
set n = len M;
set e = LineSum M;
A1: len (LineSum M) = len M by Th20;
A2: for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) >= 0 by Def6;
A3: for i being Element of NAT st i in dom (LineSum M) holds
(LineSum M) . i >= 0
proof
let i be Element of NAT ; ::_thesis: ( i in dom (LineSum M) implies (LineSum M) . i >= 0 )
assume  i in dom (LineSum M) ; ::_thesis: (LineSum M) . i >= 0
then A4: i in Seg (len M) by A1, FINSEQ_1:def_3;
then  i in dom M by FINSEQ_1:def_3;
then  for j being Nat st j in dom (Line (M,i)) holds
(Line (M,i)) . j >= 0 by A2, Lm2;
then  Sum (Line (M,i)) >= 0 by RVSUM_1:84;
hence  (LineSum M) . i >= 0 by A4, Th20; ::_thesis: verum
end;
A5: Sum (LineSum M) = SumAll M
.= 1 by Def7 ;
 len (LineSum M) = len M by Th20;
hence  ( not Row_Marginal M is empty & Row_Marginal M is ProbFinS ) by A3, A5, Def5, Th54; ::_thesis: verum
end;
cluster ColSum M ->  non empty ProbFinS ;
coherence
 ( not Column_Marginal M is empty & Column_Marginal M is ProbFinS )
proof
set e = ColSum M;
set m = width M;
A6: len (ColSum M) = width M by Def2;
A7: for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) >= 0 by Def6;
A8: for i being Element of NAT st i in dom (ColSum M) holds
(ColSum M) . i >= 0
proof
let i be Element of NAT ; ::_thesis: ( i in dom (ColSum M) implies (ColSum M) . i >= 0 )
assume  i in dom (ColSum M) ; ::_thesis: (ColSum M) . i >= 0
then A9: i in Seg (width M) by A6, FINSEQ_1:def_3;
then  for j being Nat st j in dom (Col (M,i)) holds
(Col (M,i)) . j >= 0 by A7, Lm3;
then  Sum (Col (M,i)) >= 0 by RVSUM_1:84;
hence  (ColSum M) . i >= 0 by A9, Def2; ::_thesis: verum
end;
A10: len (ColSum M) = width M by Def2;
Sum (ColSum M) = SumAll M by Th29
.= 1 by Def7 ;
hence  ( not Column_Marginal M is empty & Column_Marginal M is ProbFinS ) by A10, A8, Def5, Th54; ::_thesis: verum
end;
end;

registration
let M be non empty-yielding Matrix of REAL;
clusterM @  ->  non empty-yielding ;
coherence
 not M @ is empty-yielding
proof
A1: width M <> 0 by GOBOARD1:def_3;
then  width (M @) = len M by MATRIX_2:10;
then A2: width (M @) <> 0 by GOBOARD1:def_3;
 len (M @) <> 0 by A1, MATRIX_2:10;
hence  not M @ is empty-yielding by A2, GOBOARD1:def_3; ::_thesis: verum
end;
end;

registration
let M be non empty-yielding Joint_Probability Matrix of REAL;
clusterM @  ->  Joint_Probability ;
coherence
 M @ is Joint_Probability by Th56;
end;

theorem Th62: :: MATRPROB:62
for p being non empty ProbFinS FinSequence of REAL
for P being non empty-yielding Conditional_Probability Matrix of REAL st len p = len P holds
( p * P is non empty ProbFinS FinSequence of REAL & len (p * P) = width P )
proof
let p be non empty ProbFinS FinSequence of REAL ; ::_thesis: for P being non empty-yielding Conditional_Probability Matrix of REAL st len p = len P holds
( p * P is non empty ProbFinS FinSequence of REAL & len (p * P) = width P )
set n = len p;
let P be non empty-yielding Conditional_Probability Matrix of REAL; ::_thesis: ( len p = len P implies ( p * P is non empty ProbFinS FinSequence of REAL & len (p * P) = width P ) )
assume A1: len p = len P ; ::_thesis: ( p * P is non empty ProbFinS FinSequence of REAL & len (p * P) = width P )
A2: len (p * P) = width P by A1, MATRIXR1:62;
A3: for i being Element of NAT st i in dom (p * P) holds
(p * P) . i >= 0
proof
let i be Element of NAT ; ::_thesis: ( i in dom (p * P) implies (p * P) . i >= 0 )
assume A4: i in dom (p * P) ; ::_thesis: (p * P) . i >= 0
 i in Seg (len (p * P)) by A4, FINSEQ_1:def_3;
then A5: (p * P) . i = p "*" (Col (P,i)) by A1, Th40
.= Sum (mlt (p,(Col (P,i)))) ;
A6: for i, j being Element of NAT st [i,j] in Indices P holds
P * (i,j) >= 0 by Def6;
 i in Seg (width P) by A2, A4, FINSEQ_1:def_3;
then A7: for j being Element of NAT st j in dom (Col (P,i)) holds
(Col (P,i)) . j >= 0 by A6, Lm3;
 for i being Element of NAT st i in dom p holds
p . i >= 0 by Def5;
then  for k being Nat st k in dom (mlt (p,(Col (P,i)))) holds
(mlt (p,(Col (P,i)))) . k >= 0 by A7, Th33;
hence  (p * P) . i >= 0 by A5, RVSUM_1:84; ::_thesis: verum
end;
set m = width P;
set e = (width P) |-> 1;
A8: len ((width P) |-> 1) = width P by CARD_1:def_7;
A9: width P > 0 by Th54;
then A10: len (P @) = width P by MATRIX_2:10;
 width (P @) = len P by A9, MATRIX_2:10;
then A11: len (((width P) |-> 1) * (P @)) = len p by A1, A8, A10, MATRIXR1:62;
 for k being Nat st k in dom (((width P) |-> 1) * (P @)) holds
(((width P) |-> 1) * (P @)) . k = 1
proof
let k be Nat; ::_thesis: ( k in dom (((width P) |-> 1) * (P @)) implies (((width P) |-> 1) * (P @)) . k = 1 )
assume  k in dom (((width P) |-> 1) * (P @)) ; ::_thesis: (((width P) |-> 1) * (P @)) . k = 1
then A12: k in Seg (len (((width P) |-> 1) * (P @))) by FINSEQ_1:def_3;
then A13: k in dom P by A1, A11, FINSEQ_1:def_3;
thus (((width P) |-> 1) * (P @)) . k = Sum (Col ((P @),k)) by A8, A10, A12, Th50
.= Sum (Line (P,k)) by A13, MATRIX_2:14
.= Sum (P . k) by A13, MATRIX_2:16
.= 1 by A13, Def9 ; ::_thesis: verum
end;
then A14: ((width P) |-> 1) * (P @) = (len p) |-> 1 by A11, Th1;
Sum (p * P) = |((p * P),((width P) |-> 1))| by A2, Th32
.= |(p,(((width P) |-> 1) * (P @)))| by A1, A9, A8, Th49
.= Sum p by A14, Th32
.= 1 by Def5 ;
hence  ( p * P is non empty ProbFinS FinSequence of REAL & len (p * P) = width P ) by A2, A3, Def5, Th54; ::_thesis: verum
end;

theorem :: MATRPROB:63
for P1, P2 being non empty-yielding Conditional_Probability Matrix of REAL st width P1 = len P2 holds
( P1 * P2 is non empty-yielding Conditional_Probability Matrix of REAL & len (P1 * P2) = len P1 & width (P1 * P2) = width P2 )
proof
let P1, P2 be non empty-yielding Conditional_Probability Matrix of REAL; ::_thesis: ( width P1 = len P2 implies ( P1 * P2 is non empty-yielding Conditional_Probability Matrix of REAL & len (P1 * P2) = len P1 & width (P1 * P2) = width P2 ) )
assume A1: width P1 = len P2 ; ::_thesis: ( P1 * P2 is non empty-yielding Conditional_Probability Matrix of REAL & len (P1 * P2) = len P1 & width (P1 * P2) = width P2 )
set n2 = width P2;
set m = len P2;
set n1 = len P1;
A2: len (P1 * P2) = len P1 by A1, Th42;
A3: width (P1 * P2) = width P2 by A1, Th42;
then reconsider P = P1 * P2 as Matrix of len P1, width P2, REAL by A2, MATRIX_2:7;
A4: for i being Element of NAT st i in dom P holds
Line (P,i) is non empty ProbFinS FinSequence of REAL
proof
let i be Element of NAT ; ::_thesis: ( i in dom P implies Line (P,i) is non empty ProbFinS FinSequence of REAL )
assume  i in dom P ; ::_thesis: Line (P,i) is non empty ProbFinS FinSequence of REAL
then A5: i in Seg (len P) by FINSEQ_1:def_3;
then  i in dom P1 by A2, FINSEQ_1:def_3;
then reconsider p = Line (P1,i) as non empty ProbFinS FinSequence of REAL by Th60;
 len p = len P2 by A1, MATRIX_1:def_7;
then  p * P2 is non empty ProbFinS FinSequence of REAL by Th62;
hence  Line (P,i) is non empty ProbFinS FinSequence of REAL by A1, A5, Th42; ::_thesis: verum
end;
 ( len P1 > 0 & width P2 > 0 ) by Th54;
then  P is non empty-yielding Matrix of REAL by A2, A3, GOBOARD1:def_3;
hence  ( P1 * P2 is non empty-yielding Conditional_Probability Matrix of REAL & len (P1 * P2) = len P1 & width (P1 * P2) = width P2 ) by A1, A4, Th42, Th60; ::_thesis: verum
end;