let F, G be FinSequence of ExtREAL ; :: thesis: for a being R_eal st ( a is real or for i being Nat st i in dom F holds
F . i < 0. or for i being Nat st i in dom F holds
0. < F . i ) & dom F = dom G & ( for i being Nat st i in dom G holds
G . i = a * (F . i) ) holds
Sum G = a * (Sum F)
let a be R_eal; :: thesis: ( ( a is real or for i being Nat st i in dom F holds
F . i < 0. or for i being Nat st i in dom F holds
0. < F . i ) & dom F = dom G & ( for i being Nat st i in dom G holds
G . i = a * (F . i) ) implies Sum G = a * (Sum F) )
assume that
A1: ( a is real or for i being Nat st i in dom F holds
F . i < 0. or for i being Nat st i in dom F holds
0. < F . i ) and
A2: dom F = dom G and
A3: for i being Nat st i in dom G holds
G . i = a * (F . i) ; :: thesis: Sum G = a * (Sum F)
consider g being sequence of ExtREAL such that
A4: Sum G = g . (len G) and
A5: g . 0 = 0. and
A6: for i being Nat st i < len G holds
g . (i + 1) = (g . i) + (G . (i + 1)) by EXTREAL1:def 2;
consider f being sequence of ExtREAL such that
A7: Sum F = f . (len F) and
A8: f . 0 = 0. and
A9: for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) by EXTREAL1:def 2;
defpred S₁[ Nat] means ( $1 <= len G implies g . $1 = a * (f . $1) );
A10: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A11: S₁[i] ; :: thesis: S₁[i + 1]
assume A12: i + 1 <= len G ; :: thesis: g . (i + 1) = a * (f . (i + 1))
reconsider i = i as Element of NAT by ORDINAL1:def 12;
1 <= i + 1 by NAT_1:11;
then A13: i + 1 in dom G by A12, FINSEQ_3:25;
then i + 1 in Seg (len F) by A2, FINSEQ_1:def 3;
then i + 1 <= len F by FINSEQ_1:1;
then A14: i < len F by NAT_1:13;
i < len G by A12, NAT_1:13;
then A15: g . (i + 1) = (g . i) + (G . (i + 1)) by A6
.= (a * (f . i)) + (a * (F . (i + 1))) by A3, A11, A12, A13, NAT_1:13 ;

now :: thesis: ( ( a is real & g . (i + 1) = a * (f . (i + 1)) ) or ( ( for i being Nat st i in dom F holds
F . i < 0. ) & g . (i + 1) = a * (f . (i + 1)) ) or ( ( for i being Nat st i in dom F holds
0. < F . i ) & g . (i + 1) = a * (f . (i + 1)) ) )

per cases ( a is real or for i being Nat st i in dom F holds
F . i < 0. or for i being Nat st i in dom F holds
0. < F . i ) by A1;

case a is real ; :: thesis: g . (i + 1) = a * (f . (i + 1))

then g . (i + 1) = a * ((f . i) + (F . (i + 1))) by A15, XXREAL_3:95;
hence g . (i + 1) = a * (f . (i + 1)) by A9, A14; :: thesis: verum

end;

case A16: for i being Nat st i in dom F holds
F . i < 0. ; :: thesis: g . (i + 1) = a * (f . (i + 1))

defpred S₂[ Nat] means ( $1 < len F implies f . $1 <= 0. );
A17: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A18: S₂[i] ; :: thesis: S₂[i + 1]
assume A19: i + 1 < len F ; :: thesis: f . (i + 1) <= 0.
reconsider i = i as Element of NAT by ORDINAL1:def 12;
1 <= i + 1 by NAT_1:12;
then i + 1 in dom F by A19, FINSEQ_3:25;
then A20: F . (i + 1) < 0. by A16;
i < len F by A19, NAT_1:13;
then f . (i + 1) = (f . i) + (F . (i + 1)) by A9;
hence f . (i + 1) <= 0. by A18, A19, A20, NAT_1:13; :: thesis: verum

end;

A21: S₂[ 0 ] by A8;
for i being Nat holds S₂[i] from NAT_1:sch 2(A21, A17);
then A22: ( f . i < 0. or f . i = 0. ) by A14;
F . (i + 1) < 0. by A2, A13, A16;
then g . (i + 1) = a * ((f . i) + (F . (i + 1))) by A15, A22, XXREAL_3:97;
hence g . (i + 1) = a * (f . (i + 1)) by A9, A14; :: thesis: verum

end;

case A23: for i being Nat st i in dom F holds
0. < F . i ; :: thesis: g . (i + 1) = a * (f . (i + 1))

defpred S₂[ Nat] means ( $1 < len F implies 0. <= f . $1 );
A24: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A25: S₂[i] ; :: thesis: S₂[i + 1]
assume A26: i + 1 < len F ; :: thesis: 0. <= f . (i + 1)
reconsider i = i as Element of NAT by ORDINAL1:def 12;
1 <= i + 1 by NAT_1:12;
then i + 1 in dom F by A26, FINSEQ_3:25;
then A27: 0. < F . (i + 1) by A23;
i < len F by A26, NAT_1:13;
then f . (i + 1) = (f . i) + (F . (i + 1)) by A9;
hence 0. <= f . (i + 1) by A25, A26, A27, NAT_1:13; :: thesis: verum

end;

A28: S₂[ 0 ] by A8;
for i being Nat holds S₂[i] from NAT_1:sch 2(A28, A24);
then A29: ( 0. < f . i or f . i = 0. ) by A14;
0. < F . (i + 1) by A2, A13, A23;
then g . (i + 1) = a * ((f . i) + (F . (i + 1))) by A15, A29, XXREAL_3:96;
hence g . (i + 1) = a * (f . (i + 1)) by A9, A14; :: thesis: verum

end;

end;

end;

hence g . (i + 1) = a * (f . (i + 1)) ; :: thesis: verum

end;

A30: S₁[ 0 ] by A8, A5;
A31: for i being Nat holds S₁[i] from NAT_1:sch 2(A30, A10);
Seg (len F) = dom G by A2, FINSEQ_1:def 3
.= Seg (len G) by FINSEQ_1:def 3 ;
then a * (Sum F) = a * (f . (len G)) by A7, FINSEQ_1:6
.= g . (len G) by A31 ;
hence Sum G = a * (Sum F) by A4; :: thesis: verum