let G be FinSequence of F_Complex ; :: thesis: ( ( for i being Element of NAT st i in dom G holds
G . i is Integer ) implies Sum G is Integer )
assume A1:
for i being Element of NAT st i in dom G holds
G . i is Integer
; :: thesis: Sum G is Integer
defpred S1[ Element of NAT ] means for F being FinSequence of F_Complex st len F = $1 & ( for i being Element of NAT st i in dom F holds
F . i is Integer ) holds
Sum F is Integer;
A2:
S1[ 0 ]
A4:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
:: thesis: S1[k + 1]
let F be
FinSequence of
F_Complex ;
:: thesis: ( len F = k + 1 & ( for i being Element of NAT st i in dom F holds
F . i is Integer ) implies Sum F is Integer )
assume A6:
(
len F = k + 1 & ( for
i being
Element of
NAT st
i in dom F holds
F . i is
Integer ) )
;
:: thesis: Sum F is Integer
F <> {}
by A6;
then consider G being
FinSequence,
x being
set such that A7:
F = G ^ <*x*>
by FINSEQ_1:63;
reconsider f1 =
G as
FinSequence of
F_Complex by A7, FINSEQ_1:50;
reconsider f2 =
<*x*> as
FinSequence of
F_Complex by A7, FINSEQ_1:50;
k + 1
= (len f1) + (len f2)
by A6, A7, FINSEQ_1:35;
then A8:
k + 1
= (len f1) + 1
by FINSEQ_1:56;
A9:
for
j being
Element of
NAT st
j in dom f1 holds
f1 . j is
Integer
rng f2 c= the
carrier of
F_Complex
by FINSEQ_1:def 4;
then
{x} c= the
carrier of
F_Complex
by FINSEQ_1:55;
then reconsider m =
x as
Element of
F_Complex by ZFMISC_1:37;
A12:
F . (len F) = m
by A6, A7, A8, FINSEQ_1:59;
len F in Seg (len F)
by A6, FINSEQ_1:5;
then
len F in dom F
by FINSEQ_1:def 3;
then reconsider i2 =
m as
Integer by A6, A12;
reconsider i1 =
Sum f1 as
Integer by A5, A8, A9;
Sum F = (Sum f1) + m
by A7, FVSUM_1:87;
then
Sum F = i1 + i2
;
hence
Sum F is
Integer
;
:: thesis: verum
end;
A13:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A2, A4);
len G = len G
;
hence
Sum G is Integer
by A1, A13; :: thesis: verum