let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K

for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @))

let V1 be finite-dimensional VectSp of K; :: thesis: for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @))

defpred S_{1}[ Nat] means for M being Matrix of the carrier of V1 st len M = $1 holds

Sum (Sum M) = Sum (Sum (M @));

let M be Matrix of the carrier of V1; :: thesis: Sum (Sum M) = Sum (Sum (M @))

A1: for P being FinSequence of V1 holds Sum (Sum <*P*>) = Sum (Sum (<*P*> @))_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A36, A25);

then S_{1}[ len M]
;

hence Sum (Sum M) = Sum (Sum (M @)) ; :: thesis: verum

for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @))

let V1 be finite-dimensional VectSp of K; :: thesis: for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @))

defpred S

Sum (Sum M) = Sum (Sum (M @));

let M be Matrix of the carrier of V1; :: thesis: Sum (Sum M) = Sum (Sum (M @))

A1: for P being FinSequence of V1 holds Sum (Sum <*P*>) = Sum (Sum (<*P*> @))

proof

A25:
for n being Nat st S
defpred S_{2}[ FinSequence of V1] means Sum (Sum <*$1*>) = Sum (Sum (<*$1*> @));

let P be FinSequence of V1; :: thesis: Sum (Sum <*P*>) = Sum (Sum (<*P*> @))

len <*(<*> the carrier of V1)*> = 1 by MATRIX_0:def 2;

then width <*(<*> the carrier of V1)*> = 0 by MATRIX_0:20;

then A2: len (<*(<*> the carrier of V1)*> @) = 0 by MATRIX_0:def 6;

A3: for P being FinSequence of V1

for x being Element of V1 st S_{2}[P] holds

S_{2}[P ^ <*x*>]

then Sum (Sum <*(<*> the carrier of V1)*>) = 0. V1 by Th14

.= Sum (Sum (<*(<*> the carrier of V1)*> @)) by A2, Th13 ;

then A24: S_{2}[ <*> the carrier of V1]
;

for P being FinSequence of V1 holds S_{2}[P]
from FINSEQ_2:sch 2(A24, A3);

hence Sum (Sum <*P*>) = Sum (Sum (<*P*> @)) ; :: thesis: verum

end;let P be FinSequence of V1; :: thesis: Sum (Sum <*P*>) = Sum (Sum (<*P*> @))

len <*(<*> the carrier of V1)*> = 1 by MATRIX_0:def 2;

then width <*(<*> the carrier of V1)*> = 0 by MATRIX_0:20;

then A2: len (<*(<*> the carrier of V1)*> @) = 0 by MATRIX_0:def 6;

A3: for P being FinSequence of V1

for x being Element of V1 st S

S

proof

<*(<*> the carrier of V1)*> is Matrix of 0 + 1, 0 , the carrier of V1
;
let P be FinSequence of V1; :: thesis: for x being Element of V1 st S_{2}[P] holds

S_{2}[P ^ <*x*>]

let x be Element of V1; :: thesis: ( S_{2}[P] implies S_{2}[P ^ <*x*>] )

assume A4: Sum (Sum <*P*>) = Sum (Sum (<*P*> @)) ; :: thesis: S_{2}[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 A5: len (<*P*> ^^ <*<*x*>*>) = 1 by FINSEQ_1:6

.= len <*(P ^ <*x*>)*> by FINSEQ_1:39 ;

then A6: dom (<*P*> ^^ <*<*x*>*>) = Seg (len <*(P ^ <*x*>)*>) by FINSEQ_1:def 3;

end;S

let x be Element of V1; :: thesis: ( S

assume A4: Sum (Sum <*P*>) = Sum (Sum (<*P*> @)) ; :: thesis: S

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 A5: len (<*P*> ^^ <*<*x*>*>) = 1 by FINSEQ_1:6

.= len <*(P ^ <*x*>)*> by FINSEQ_1:39 ;

then A6: dom (<*P*> ^^ <*<*x*>*>) = Seg (len <*(P ^ <*x*>)*>) by FINSEQ_1:def 3;

A7: now :: thesis: for i being Nat st i in dom (<*P*> ^^ <*<*x*>*>) holds

(<*P*> ^^ <*<*x*>*>) . i = <*(P ^ <*x*>)*> . i

(<*P*> ^^ <*<*x*>*>) . i = <*(P ^ <*x*>)*> . i

let i be Nat; :: thesis: ( i in dom (<*P*> ^^ <*<*x*>*>) implies (<*P*> ^^ <*<*x*>*>) . i = <*(P ^ <*x*>)*> . i )

assume A8: i in dom (<*P*> ^^ <*<*x*>*>) ; :: thesis: (<*P*> ^^ <*<*x*>*>) . i = <*(P ^ <*x*>)*> . i

then i in {1} by A6, FINSEQ_1:2, FINSEQ_1:40;

then A9: i = 1 by TARSKI:def 1;

reconsider m1 = <*P*> . i, m2 = <*<*x*>*> . i as FinSequence ;

thus (<*P*> ^^ <*<*x*>*>) . i = m1 ^ m2 by A8, PRE_POLY:def 4

.= P ^ m2 by A9, FINSEQ_1:40

.= P ^ <*x*> by A9, FINSEQ_1:40

.= <*(P ^ <*x*>)*> . i by A9, FINSEQ_1:40 ; :: thesis: verum

end;assume A8: i in dom (<*P*> ^^ <*<*x*>*>) ; :: thesis: (<*P*> ^^ <*<*x*>*>) . i = <*(P ^ <*x*>)*> . i

then i in {1} by A6, FINSEQ_1:2, FINSEQ_1:40;

then A9: i = 1 by TARSKI:def 1;

reconsider m1 = <*P*> . i, m2 = <*<*x*>*> . i as FinSequence ;

thus (<*P*> ^^ <*<*x*>*>) . i = m1 ^ m2 by A8, PRE_POLY:def 4

.= P ^ m2 by A9, FINSEQ_1:40

.= P ^ <*x*> by A9, FINSEQ_1:40

.= <*(P ^ <*x*>)*> . i by A9, FINSEQ_1:40 ; :: thesis: verum

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

end;

suppose
len P = 0
; :: thesis: S_{2}[P ^ <*x*>]

then A10:
P = {}
;

hence Sum (Sum <*(P ^ <*x*>)*>) = Sum (Sum <*<*x*>*>) by FINSEQ_1:34

.= Sum (Sum (<*<*x*>*> @)) by Th15

.= Sum (Sum (<*(P ^ <*x*>)*> @)) by A10, FINSEQ_1:34 ;

:: thesis: verum

end;hence Sum (Sum <*(P ^ <*x*>)*>) = Sum (Sum <*<*x*>*>) by FINSEQ_1:34

.= Sum (Sum (<*<*x*>*> @)) by Th15

.= Sum (Sum (<*(P ^ <*x*>)*> @)) by A10, FINSEQ_1:34 ;

:: thesis: verum

suppose A11:
len P <> 0
; :: thesis: S_{2}[P ^ <*x*>]

A12:
len <*<*x*>*> = 1
by FINSEQ_1:40;

then A13: width <*<*x*>*> = len <*x*> by MATRIX_0:20

.= 1 by FINSEQ_1:40 ;

then A14: len (<*<*x*>*> @) = 1 by MATRIX_0:def 6;

A15: len <*P*> = 1 by FINSEQ_1:40;

then A16: width <*P*> = len P by MATRIX_0:20;

then A17: len (<*P*> @) = len P by MATRIX_0:def 6;

width (<*P*> @) = 1 by A11, A15, A16, MATRIX_0:54;

then reconsider d1 = <*P*> @ as Matrix of len P,1, the carrier of V1 by A11, A17, MATRIX_0:20;

A18: len <*(P ^ <*x*>)*> = 1 by FINSEQ_1:40;

then A19: 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 ;

A20: (<*<*x*>*> @) @ = <*<*x*>*> by A12, A13, MATRIX_0:57;

A21: width (<*P*> @) = len <*P*> by A11, A16, MATRIX_0:54

.= width (<*<*x*>*> @) by A15, A12, A13, MATRIX_0:54 ;

then width (<*<*x*>*> @) = 1 by A11, A15, A16, MATRIX_0:54;

then reconsider d2 = <*<*x*>*> @ as Matrix of 1,1, the carrier of V1 by A14, MATRIX_0:20;

A22: (d1 ^ d2) @ = ((<*P*> @) @) ^^ ((<*<*x*>*> @) @) by A21, Th28

.= <*P*> ^^ <*<*x*>*> by A11, A15, A16, A20, MATRIX_0:57

.= <*(P ^ <*x*>)*> by A5, A7, FINSEQ_2:9

.= (<*(P ^ <*x*>)*> @) @ by A18, A19, MATRIX_0:57 ;

A23: 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 A16, A13, A19, MATRIX_0:def 6 ;

thus Sum (Sum <*(P ^ <*x*>)*>) = Sum (Sum (<*P*> ^^ <*<*x*>*>)) by A5, A7, FINSEQ_2:9

.= (Sum (Sum (<*P*> @))) + (Sum (Sum <*<*x*>*>)) by A4, A15, A12, Th31

.= (Sum (Sum (<*P*> @))) + (Sum (Sum (<*<*x*>*> @))) by Th15

.= Sum ((Sum d1) ^ (Sum d2)) by RLVECT_1:41

.= Sum (Sum (d1 ^ d2)) by Th27

.= Sum (Sum (<*(P ^ <*x*>)*> @)) by A23, A22, MATRIX_0:53 ; :: thesis: verum

end;then A13: width <*<*x*>*> = len <*x*> by MATRIX_0:20

.= 1 by FINSEQ_1:40 ;

then A14: len (<*<*x*>*> @) = 1 by MATRIX_0:def 6;

A15: len <*P*> = 1 by FINSEQ_1:40;

then A16: width <*P*> = len P by MATRIX_0:20;

then A17: len (<*P*> @) = len P by MATRIX_0:def 6;

width (<*P*> @) = 1 by A11, A15, A16, MATRIX_0:54;

then reconsider d1 = <*P*> @ as Matrix of len P,1, the carrier of V1 by A11, A17, MATRIX_0:20;

A18: len <*(P ^ <*x*>)*> = 1 by FINSEQ_1:40;

then A19: 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 ;

A20: (<*<*x*>*> @) @ = <*<*x*>*> by A12, A13, MATRIX_0:57;

A21: width (<*P*> @) = len <*P*> by A11, A16, MATRIX_0:54

.= width (<*<*x*>*> @) by A15, A12, A13, MATRIX_0:54 ;

then width (<*<*x*>*> @) = 1 by A11, A15, A16, MATRIX_0:54;

then reconsider d2 = <*<*x*>*> @ as Matrix of 1,1, the carrier of V1 by A14, MATRIX_0:20;

A22: (d1 ^ d2) @ = ((<*P*> @) @) ^^ ((<*<*x*>*> @) @) by A21, Th28

.= <*P*> ^^ <*<*x*>*> by A11, A15, A16, A20, MATRIX_0:57

.= <*(P ^ <*x*>)*> by A5, A7, FINSEQ_2:9

.= (<*(P ^ <*x*>)*> @) @ by A18, A19, MATRIX_0:57 ;

A23: 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 A16, A13, A19, MATRIX_0:def 6 ;

thus Sum (Sum <*(P ^ <*x*>)*>) = Sum (Sum (<*P*> ^^ <*<*x*>*>)) by A5, A7, FINSEQ_2:9

.= (Sum (Sum (<*P*> @))) + (Sum (Sum <*<*x*>*>)) by A4, A15, A12, Th31

.= (Sum (Sum (<*P*> @))) + (Sum (Sum (<*<*x*>*> @))) by Th15

.= Sum ((Sum d1) ^ (Sum d2)) by RLVECT_1:41

.= Sum (Sum (d1 ^ d2)) by Th27

.= Sum (Sum (<*(P ^ <*x*>)*> @)) by A23, A22, MATRIX_0:53 ; :: thesis: verum

then Sum (Sum <*(<*> the carrier of V1)*>) = 0. V1 by Th14

.= Sum (Sum (<*(<*> the carrier of V1)*> @)) by A2, Th13 ;

then A24: S

for P being FinSequence of V1 holds S

hence Sum (Sum <*P*>) = Sum (Sum (<*P*> @)) ; :: thesis: verum

S

proof

A36:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A26: for M being Matrix of the carrier of V1 st len M = n holds

Sum (Sum M) = Sum (Sum (M @)) ; :: thesis: S_{1}[n + 1]

thus for M being Matrix of the carrier of V1 st len M = n + 1 holds

Sum (Sum M) = Sum (Sum (M @)) :: thesis: verum

end;assume A26: for M being Matrix of the carrier of V1 st len M = n holds

Sum (Sum M) = Sum (Sum (M @)) ; :: thesis: S

thus for M being Matrix of the carrier of V1 st len M = n + 1 holds

Sum (Sum M) = Sum (Sum (M @)) :: thesis: verum

proof

let M be Matrix of the carrier of V1; :: thesis: ( len M = n + 1 implies Sum (Sum M) = Sum (Sum (M @)) )

assume A27: len M = n + 1 ; :: thesis: Sum (Sum M) = Sum (Sum (M @))

A28: M <> {} by A27;

A29: dom M = Seg (len M) by FINSEQ_1:def 3;

end;assume A27: len M = n + 1 ; :: thesis: Sum (Sum M) = Sum (Sum (M @))

A28: M <> {} by A27;

A29: dom M = Seg (len M) by FINSEQ_1:def 3;

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

end;

suppose A30:
n = 0
; :: thesis: Sum (Sum M) = Sum (Sum (M @))

then
M . 1 = Line (M,1)
by A27, A29, FINSEQ_1:4, MATRIX_0:60;

then reconsider G = M . 1 as FinSequence of V1 ;

M = <*G*> by A27, A30, FINSEQ_1:40;

hence Sum (Sum M) = Sum (Sum (M @)) by A1; :: thesis: verum

end;then reconsider G = M . 1 as FinSequence of V1 ;

M = <*G*> by A27, A30, FINSEQ_1:40;

hence Sum (Sum M) = Sum (Sum (M @)) by A1; :: thesis: verum

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

A32:
M . (n + 1) = Line (M,(n + 1))
by A27, A29, FINSEQ_1:4, MATRIX_0:60;

then reconsider M1 = M . (n + 1) as FinSequence of V1 ;

len M1 = width M by A32, MATRIX_0:def 7;

then reconsider R = <*M1*> as Matrix of 1, width M, the carrier of V1 ;

reconsider M9 = M as Matrix of n + 1, width M, the carrier of V1 by A27, MATRIX_0:20;

reconsider W = Del (M9,(n + 1)) as Matrix of n, width M, the carrier of V1 by Th3;

A33: width W = width M9 by A31, Th2

.= width R by Th2 ;

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 A27, Th1;

thus Sum (Sum M) = Sum (Sum (W ^ R)) by A28, Th4, A27

.= Sum ((Sum W) ^ (Sum R)) by Th27

.= (Sum (Sum (Del (M,(n + 1))))) + (Sum (Sum R)) by RLVECT_1:41

.= (Sum (Sum ((Del (M,(n + 1))) @))) + (Sum (Sum R)) by A26, A35

.= (Sum (Sum ((Del (M,(n + 1))) @))) + (Sum (Sum (R @))) by A1

.= Sum (Sum ((W @) ^^ (R @))) by A34, Th31

.= Sum (Sum ((W ^ R) @)) by A33, Th28

.= Sum (Sum (M @)) by A28, Th4, A27 ; :: thesis: verum

end;then reconsider M1 = M . (n + 1) as FinSequence of V1 ;

len M1 = width M by A32, MATRIX_0:def 7;

then reconsider R = <*M1*> as Matrix of 1, width M, the carrier of V1 ;

reconsider M9 = M as Matrix of n + 1, width M, the carrier of V1 by A27, MATRIX_0:20;

reconsider W = Del (M9,(n + 1)) as Matrix of n, width M, the carrier of V1 by Th3;

A33: width W = width M9 by A31, Th2

.= width R by Th2 ;

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 A27, Th1;

thus Sum (Sum M) = Sum (Sum (W ^ R)) by A28, Th4, A27

.= Sum ((Sum W) ^ (Sum R)) by Th27

.= (Sum (Sum (Del (M,(n + 1))))) + (Sum (Sum R)) by RLVECT_1:41

.= (Sum (Sum ((Del (M,(n + 1))) @))) + (Sum (Sum R)) by A26, A35

.= (Sum (Sum ((Del (M,(n + 1))) @))) + (Sum (Sum (R @))) by A1

.= Sum (Sum ((W @) ^^ (R @))) by A34, Th31

.= Sum (Sum ((W ^ R) @)) by A33, Th28

.= Sum (Sum (M @)) by A28, Th4, A27 ; :: thesis: verum

proof

for n being Nat holds S
let M be Matrix of the carrier of V1; :: thesis: ( len M = 0 implies Sum (Sum M) = Sum (Sum (M @)) )

assume A37: len M = 0 ; :: thesis: Sum (Sum M) = Sum (Sum (M @))

then width M = 0 by MATRIX_0:def 3;

then A38: len (M @) = 0 by MATRIX_0:def 6;

thus Sum (Sum M) = 0. V1 by A37, Th13

.= Sum (Sum (M @)) by A38, Th13 ; :: thesis: verum

end;assume A37: len M = 0 ; :: thesis: Sum (Sum M) = Sum (Sum (M @))

then width M = 0 by MATRIX_0:def 3;

then A38: len (M @) = 0 by MATRIX_0:def 6;

thus Sum (Sum M) = 0. V1 by A37, Th13

.= Sum (Sum (M @)) by A38, Th13 ; :: thesis: verum

then S

hence Sum (Sum M) = Sum (Sum (M @)) ; :: thesis: verum