let M be Matrix of REAL; :: thesis: SumAll M = SumAll (M @)
defpred S₁[ 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 S₂[ 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 S₂[p] holds
S₂[p ^ <*x*>]

proof

let p be FinSequence of REAL ; :: thesis: for x being Element of REAL st S₂[p] holds
S₂[p ^ <*x*>]
let x be Element of REAL ; :: thesis: ( S₂[p] implies S₂[p ^ <*x*>] )
assume A3: SumAll <*p*> = SumAll (<*p*> @) ; :: thesis: S₂[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
.= p ^ <*x*> by A8
.= <*(p ^ <*x*>)*> . i by A8 ;
:: thesis: verum

end;

per cases ( len p = 0 or len p <> 0 ) ;

suppose len p = 0 ; :: thesis: S₂[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;

suppose A10: len p <> 0 ; :: thesis: S₂[p ^ <*x*>]

A11: len <*<*x*>*> = 1 by FINSEQ_1:40;
then A12: width <*<*x*>*> = len <*x*> by MATRIX_0:20
.= 1 by FINSEQ_1:40 ;
then A13: len (<*<*x*>*> @) = 1 by MATRIX_0:def 6;
A14: len <*p*> = 1 by FINSEQ_1:40;
then A15: width <*p*> = len p by MATRIX_0:20;
then A16: len (<*p*> @) = len p by MATRIX_0:def 6;
width (<*p*> @) = 1 by A10, A14, A15, MATRIX_0:54;
then reconsider d1 = <*p*> @ as Matrix of len p,1,REAL by A10, A16, MATRIX_0:20;
len <*(p ^ <*x*>)*> = 1 by FINSEQ_1:40;
then A17: width <*(p ^ <*x*>)*> = len (p ^ <*x*>) by MATRIX_0:20
.= (len p) + (len <*x*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
A18: (<*<*x*>*> @) @ = <*<*x*>*> by A11, A12, MATRIX_0:57;
A19: width (<*p*> @) = len <*p*> by A10, A15, MATRIX_0:54
.= width (<*<*x*>*> @) by A14, A11, A12, MATRIX_0:54 ;
then width (<*<*x*>*> @) = 1 by A10, A14, A15, MATRIX_0:54;
then reconsider d2 = <*<*x*>*> @ as Matrix of 1,1,REAL by A13, MATRIX_0:20;
A20: (d1 ^ d2) @ = ((<*p*> @) @) ^^ ((<*<*x*>*> @) @) by A19, MATRLIN:28
.= <*p*> ^^ <*<*x*>*> by A10, A14, A15, A18, MATRIX_0:57
.= <*(p ^ <*x*>)*> by A4, A6, FINSEQ_2:9
.= (<*(p ^ <*x*>)*> @) @ by A17, MATRIX_0:57 ;
A21: len ((<*p*> @) ^ (<*<*x*>*> @)) = (len (<*p*> @)) + (len (<*<*x*>*> @)) by FINSEQ_1:22
.= (width <*p*>) + (len (<*<*x*>*> @)) by MATRIX_0:def 6
.= (width <*p*>) + (width <*<*x*>*>) by MATRIX_0:def 6
.= len (<*(p ^ <*x*>)*> @) by A15, A12, A17, MATRIX_0: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 A21, A20, MATRIX_0:53 ; :: thesis: verum

end;

end;

end;

A22: S₂[ <*> REAL]

proof

set M1 = <*(<*> REAL)*>;
reconsider E = <*> REAL as Element of REAL * by FINSEQ_1:def 11;
set M1 = <*E*>;
reconsider M1 = <*E*> as Matrix of REAL by MATRIX_0:3;
A23: len M1 = 1 by FINSEQ_1:39;
for p being FinSequence of REAL st p in rng M1 holds
len p = 0

proof

let p be FinSequence of REAL ; :: thesis: ( p in rng M1 implies len p = 0 )
assume A24: p in rng M1 ; :: thesis: len p = 0
rng M1 = {(<*> REAL)} by FINSEQ_1:38;
then p = <*> REAL by A24, TARSKI:def 1;
hence len p = 0 ; :: thesis: verum

end;

then M1 is 1, 0 -size by A23, MATRIX_0:def 2;
then reconsider M1 = M1 as Matrix of 1, 0 ,REAL ;
A25: width M1 = 0 by MATRIX_0:20, A23;
A26: len (M1 @) = 0 by MATRIX_0:def 6, A25;
SumAll M1 = 0 by Th24
.= SumAll (M1 @) by A26, Th23 ;
hence S₂[ <*> REAL] ; :: thesis: verum

end;

for p being FinSequence of REAL holds S₂[p] from FINSEQ_2:sch 2(A22, A2);
hence SumAll <*p*> = SumAll (<*p*> @) ; :: thesis: verum

end;

A27: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A28: for M being Matrix of REAL st len M = n holds
SumAll M = SumAll (M @) ; :: thesis: S₁[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 A29: len M = n + 1 ; :: thesis: SumAll M = SumAll (M @)
a29: M <> {} by A29;
A30: dom M = Seg (len M) by FINSEQ_1:def 3;

per cases ( n = 0 or n > 0 ) ;

suppose A31: n = 0 ; :: thesis: SumAll M = SumAll (M @)

reconsider g = M . 1 as FinSequence of REAL ;
M = <*g*> by A29, A31, FINSEQ_1:40;
hence SumAll M = SumAll (M @) by A1; :: thesis: verum

end;

suppose A32: n > 0 ; :: thesis: SumAll M = SumAll (M @)

reconsider M9 = M as Matrix of n + 1, width M,REAL by A29, MATRIX_0: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 A29, A30, FINSEQ_1:4, MATRIX_0:60;
then len M1 = width M by MATRIX_0:def 7;
then reconsider r = <*M1*> as Matrix of 1, width M,REAL ;
A33: width w = width M9 by A32, MATRLIN:2
.= width r by MATRLIN:2 ;
A34: len (w @) = width w by MATRIX_0:def 6
.= len (r @) by A33, MATRIX_0:def 6 ;
A35: len (Del (M,(n + 1))) = n by A29, PRE_POLY:12;
thus SumAll M = SumAll (w ^ r) by a29, A29, 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 A28, A35
.= (SumAll ((Del (M,(n + 1))) @)) + (SumAll (r @)) by A1
.= SumAll ((w @) ^^ (r @)) by A34, Th27
.= SumAll ((w ^ r) @) by A33, MATRLIN:28
.= SumAll (M @) by a29, PRE_POLY:13, A29 ; :: thesis: verum

end;

end;

end;

end;

A36: S₁[ 0 ]

proof

let M be Matrix of REAL; :: thesis: ( len M = 0 implies SumAll M = SumAll (M @) )
assume A37: len M = 0 ; :: thesis: SumAll M = SumAll (M @)
then width M = 0 by MATRIX_0:def 3;
then A38: len (M @) = 0 by MATRIX_0:def 6;
thus SumAll M = 0 by A37, Th23
.= SumAll (M @) by A38, Th23 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A36, A27);
then S₁[ len M] ;
hence SumAll M = SumAll (M @) ; :: thesis: verum