defpred S₁[ FinSequence of ExtREAL ] means ( not -infty in rng $1 implies SumAll <*$1*> = SumAll (<*$1*> @) );
let p be FinSequence of ExtREAL ; :: thesis: ( not -infty in rng p implies SumAll <*p*> = SumAll (<*p*> @) )
assume B0: not -infty in rng p ; :: thesis: SumAll <*p*> = SumAll (<*p*> @)
A2: for p being FinSequence of ExtREAL
for x being Element of ExtREAL st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of ExtREAL ; :: thesis: for x being Element of ExtREAL st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of ExtREAL ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A3: ( not -infty in rng p implies SumAll <*p*> = SumAll (<*p*> @) ) ; :: thesis: S₁[p ^ <*x*>]
assume not -infty in rng (p ^ <*x*>) ; :: thesis: SumAll <*(p ^ <*x*>)*> = SumAll (<*(p ^ <*x*>)*> @)
then not -infty in (rng p) \/ (rng <*x*>) by FINSEQ_1:31;
then B3: ( not -infty in rng p & not -infty in rng <*x*> ) by XBOOLE_0:def 3;
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 A8: i = 1 by FINSEQ_1:90;
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: SumAll <*(p ^ <*x*>)*> = SumAll (<*(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: SumAll <*(p ^ <*x*>)*> = SumAll (<*(p ^ <*x*>)*> @)

A11: ( len <*<*x*>*> = 1 & len <*p*> = 1 & len <*x*> = 1 ) by FINSEQ_1:40;
then A12: ( width <*<*x*>*> = 1 & width <*p*> = len p ) by MATRIX_0:20;
then A16: len (<*p*> @) = len p by MATRIX_0:def 6;
P5: width (<*p*> @) = 1 by A10, A11, A12, MATRIX_0:29;
then reconsider d1 = <*p*> @ as Matrix of len p,1,ExtREAL by A10, A16, MATRIX_0:20;
A13: len (<*<*x*>*> @) = 1 by A12, MATRIX_0:54;
PP5: width (<*<*x*>*> @) = 1 by A11, A12, MATRIX_0:29;
then reconsider d2 = <*<*x*>*> @ as Matrix of 1,1,ExtREAL by A13, MATRIX_0:20;
len <*(p ^ <*x*>)*> = 1 by FINSEQ_1:40;
then A18: width <*(p ^ <*x*>)*> = len (p ^ <*x*>) by MATRIX_0:20
.= (len p) + 1 by A11, FINSEQ_1:22 ;
A19: (<*<*x*>*> @) @ = <*<*x*>*> by A11, A12, MATRIX_0:57;
width (<*p*> @) = width (<*<*x*>*> @) by P5, A11, A12, MATRIX_0:29;
then A21: (d1 ^ d2) @ = ((<*p*> @) @) ^^ ((<*<*x*>*> @) @) by MATRLIN:28
.= <*p*> ^^ <*<*x*>*> by A10, A11, A12, A19, MATRIX_0:57
.= <*(p ^ <*x*>)*> by A4, A6, FINSEQ_2:9
.= (<*(p ^ <*x*>)*> @) @ by A18, MATRIX_0:57 ;
A22: 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 A12, A18, MATRIX_0:def 6 ;

B4: now :: thesis: for i being Nat st i in dom <*p*> holds
not -infty in rng (<*p*> . i)

let i be Nat; :: thesis: ( i in dom <*p*> implies not -infty in rng (<*p*> . i) )
assume i in dom <*p*> ; :: thesis: not -infty in rng (<*p*> . i)
then i = 1 by FINSEQ_1:90;
hence not -infty in rng (<*p*> . i) by B3; :: thesis: verum

end;

B5: now :: thesis: for i being Nat st i in dom <*<*x*>*> holds
not -infty in rng (<*<*x*>*> . i)

let i be Nat; :: thesis: ( i in dom <*<*x*>*> implies not -infty in rng (<*<*x*>*> . i) )
assume i in dom <*<*x*>*> ; :: thesis: not -infty in rng (<*<*x*>*> . i)
then i = 1 by FINSEQ_1:90;
hence not -infty in rng (<*<*x*>*> . i) by B3; :: thesis: verum

end;

dom <*p*> = Seg 1 by FINSEQ_1:38;
then 1 in dom <*p*> ;
then B6: not -infty in rng (<*p*> . 1) by B4;
then T6: not -infty in rng p ;
for x being object st x in dom (Sum d1) holds
(Sum d1) . x <> -infty

proof

let x be object ; :: thesis: ( x in dom (Sum d1) implies (Sum d1) . x <> -infty )
assume P1: x in dom (Sum d1) ; :: thesis: (Sum d1) . x <> -infty
then reconsider i = x as Nat ;
P2: (Sum d1) . x = Sum (d1 . i) by P1, Def5;
( 1 <= i & i <= len (Sum d1) ) by P1, FINSEQ_3:25;
then P3: ( 1 <= i & i <= len d1 ) by Def5;
then i in dom p by A16, FINSEQ_3:25;
then R10: p . i <> -infty by T6, FUNCT_1:3;
i in dom d1 by P3, FINSEQ_3:25;
then P4: d1 . i = Line (d1,i) by MATRIX_0:60;
dom d1 = Seg (len p) by A16, FINSEQ_1:def 3;
then R2: Indices d1 = [:(Seg (len p)),{1}:] by P5, FINSEQ_1:2, MATRIX_0:def 4;
R3: i in Seg (len p) by P3, A16;
for j being Nat st j in dom (Line (d1,i)) holds
(Line (d1,i)) . j <> -infty

proof

let j be Nat; :: thesis: ( j in dom (Line (d1,i)) implies (Line (d1,i)) . j <> -infty )
assume j in dom (Line (d1,i)) ; :: thesis: (Line (d1,i)) . j <> -infty
then ( 1 <= j & j <= len (Line (d1,i)) ) by FINSEQ_3:25;
then ( 1 <= j & j <= width d1 ) by MATRIX_0:def 7;
then P6: j in Seg (width d1) ;
then R4: [i,j] in [:(Seg (len p)),{1}:] by P5, R3, FINSEQ_1:2, ZFMISC_1:def 2;
then [j,i] in Indices (d1 @) by R2, MATRIX_0:def 6;
then consider F being FinSequence of ExtREAL such that
R7: ( F = (d1 @) . j & (d1 @) * (j,i) = F . i ) by MATRIX_0:def 5;
F = <*p*> . j by A10, A12, R7, A11, MATRIX_0:57;
then F = <*p*> . 1 by P5, P6, FINSEQ_1:2, TARSKI:def 1;
then R9: F = p ;
(Line (d1,i)) . j = (<*p*> @) * (i,j) by P6, MATRIX_0:def 7;
hence (Line (d1,i)) . j <> -infty by R7, R9, R10, R2, R4, MATRIX_0:def 6; :: thesis: verum

end;

hence (Sum d1) . x <> -infty by P2, P4, Th17; :: thesis: verum

end;

then B7: not -infty in rng (Sum d1) by FUNCT_1:def 3;
for z being object st z in dom (Sum d2) holds
(Sum d2) . z <> -infty

proof

let z be object ; :: thesis: ( z in dom (Sum d2) implies (Sum d2) . z <> -infty )
assume P1: z in dom (Sum d2) ; :: thesis: (Sum d2) . z <> -infty
then reconsider i = z as Nat ;
P2: (Sum d2) . z = Sum (d2 . i) by P1, Def5;
( 1 <= i & i <= len (Sum d2) ) by P1, FINSEQ_3:25;
then P3: ( 1 <= i & i <= len d2 ) by Def5;
then R1: ( 1 <= i & i <= len <*x*> ) by A13, FINSEQ_1:40;
then i in dom <*x*> by FINSEQ_3:25;
then R10: <*x*> . i <> -infty by B3, FUNCT_1:3;
i in dom d2 by P3, FINSEQ_3:25;
then P4: d2 . i = Line (d2,i) by MATRIX_0:60;
dom d2 = Seg (len <*x*>) by A13, FINSEQ_1:def 3, FINSEQ_1:40;
then R2: Indices d2 = [:(Seg (len <*x*>)),{1}:] by PP5, FINSEQ_1:2, MATRIX_0:def 4;
R3: i in Seg (len <*x*>) by R1;
for j being Nat st j in dom (Line (d2,i)) holds
(Line (d2,i)) . j <> -infty

proof

let j be Nat; :: thesis: ( j in dom (Line (d2,i)) implies (Line (d2,i)) . j <> -infty )
assume j in dom (Line (d2,i)) ; :: thesis: (Line (d2,i)) . j <> -infty
then ( 1 <= j & j <= len (Line (d2,i)) ) by FINSEQ_3:25;
then ( 1 <= j & j <= width d2 ) by MATRIX_0:def 7;
then P6: j in Seg (width d2) ;
then R4: [i,j] in [:(Seg (len <*x*>)),{1}:] by PP5, R3, FINSEQ_1:2, ZFMISC_1:def 2;
then [j,i] in Indices (d2 @) by R2, MATRIX_0:def 6;
then consider F being FinSequence of ExtREAL such that
R7: ( F = (d2 @) . j & (d2 @) * (j,i) = F . i ) by MATRIX_0:def 5;
F = <*<*x*>*> . j by A12, R7, A11, MATRIX_0:57;
then F = <*<*x*>*> . 1 by PP5, P6, FINSEQ_1:2, TARSKI:def 1;
then R9: F = <*x*> ;
(Line (d2,i)) . j = (<*<*x*>*> @) * (i,j) by P6, MATRIX_0:def 7;
hence (Line (d2,i)) . j <> -infty by R7, R9, R10, R2, R4, MATRIX_0:def 6; :: thesis: verum

end;

hence (Sum d2) . z <> -infty by P2, P4, Th17; :: thesis: verum

end;

then B8: not -infty in rng (Sum d2) by FUNCT_1:def 3;
thus SumAll <*(p ^ <*x*>)*> = SumAll (<*p*> ^^ <*<*x*>*>) by A4, A6, FINSEQ_2:9
.= (SumAll <*p*>) + (SumAll <*<*x*>*>) by A11, B4, B5, Th25
.= (SumAll (<*p*> @)) + (SumAll (<*<*x*>*> @)) by A3, B6, MATRLIN:15
.= Sum ((Sum d1) ^ (Sum d2)) by B7, B8, EXTREAL1:10
.= SumAll (d1 ^ d2) by Th23
.= SumAll (<*(p ^ <*x*>)*> @) by A22, A21, MATRIX_0:53 ; :: thesis: verum

end;

end;

end;

A23: S₁[ <*> ExtREAL]

proof

reconsider M1 = <*(<*> ExtREAL)*> as Matrix of 1, 0 ,ExtREAL by MATRIX_0:14;
len M1 = 1 by MATRIX_0:def 2;
then width M1 = 0 by MATRIX_0:20;
then A24: len (M1 @) = 0 by MATRIX_0:def 6;
SumAll M1 = 0 by Th22;
hence S₁[ <*> ExtREAL] by A24, Th21; :: thesis: verum

end;

for p being FinSequence of ExtREAL holds S₁[p] from FINSEQ_2:sch 2(A23, A2);
hence SumAll <*p*> = SumAll (<*p*> @) by B0; :: thesis: verum