defpred S_{1}[ 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;

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

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A11, A2);

len G = len G ;

hence Sum G is Integer by A1, A13; :: thesis: verum

F . i is Integer ) holds

Sum F is Integer;

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

A2: for k being Nat st S

S

proof

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

assume A3: S_{1}[k]
; :: thesis: S_{1}[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 that

A4: len F = k + 1 and

A5: for i being Element of NAT st i in dom F holds

F . i is Integer ; :: thesis: Sum F is Integer

F <> {} by A4;

then consider G being FinSequence, x being object such that

A6: F = G ^ <*x*> by FINSEQ_1:46;

len F in Seg (len F) by A4, FINSEQ_1:3;

then A7: len F in dom F by FINSEQ_1:def 3;

reconsider f2 = <*x*> as FinSequence of F_Complex by A6, FINSEQ_1:36;

reconsider f1 = G as FinSequence of F_Complex by A6, FINSEQ_1:36;

rng f2 c= the carrier of F_Complex by FINSEQ_1:def 4;

then {x} c= the carrier of F_Complex by FINSEQ_1:38;

then reconsider m = x as Element of F_Complex by ZFMISC_1:31;

k + 1 = (len f1) + (len f2) by A4, A6, FINSEQ_1:22;

then A8: k + 1 = (len f1) + 1 by FINSEQ_1:39;

then F . (len F) = m by A4, A6, FINSEQ_1:42;

then reconsider i2 = m as Integer by A5, A7;

for j being Element of NAT st j in dom f1 holds

f1 . j is Integer

Sum F = (Sum f1) + m by A6, FVSUM_1:71;

then Sum F = i1 + i2 ;

hence Sum F is Integer ; :: thesis: verum

end;assume A3: S

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 that

A4: len F = k + 1 and

A5: for i being Element of NAT st i in dom F holds

F . i is Integer ; :: thesis: Sum F is Integer

F <> {} by A4;

then consider G being FinSequence, x being object such that

A6: F = G ^ <*x*> by FINSEQ_1:46;

len F in Seg (len F) by A4, FINSEQ_1:3;

then A7: len F in dom F by FINSEQ_1:def 3;

reconsider f2 = <*x*> as FinSequence of F_Complex by A6, FINSEQ_1:36;

reconsider f1 = G as FinSequence of F_Complex by A6, FINSEQ_1:36;

rng f2 c= the carrier of F_Complex by FINSEQ_1:def 4;

then {x} c= the carrier of F_Complex by FINSEQ_1:38;

then reconsider m = x as Element of F_Complex by ZFMISC_1:31;

k + 1 = (len f1) + (len f2) by A4, A6, FINSEQ_1:22;

then A8: k + 1 = (len f1) + 1 by FINSEQ_1:39;

then F . (len F) = m by A4, A6, FINSEQ_1:42;

then reconsider i2 = m as Integer by A5, A7;

for j being Element of NAT st j in dom f1 holds

f1 . j is Integer

proof

then reconsider i1 = Sum f1 as Integer by A3, A8;
A9:
dom f1 c= dom F
by A6, FINSEQ_1:26;

let j be Element of NAT ; :: thesis: ( j in dom f1 implies f1 . j is Integer )

assume A10: j in dom f1 ; :: thesis: f1 . j is Integer

F . j = f1 . j by A6, A10, FINSEQ_1:def 7;

hence f1 . j is Integer by A5, A10, A9; :: thesis: verum

end;let j be Element of NAT ; :: thesis: ( j in dom f1 implies f1 . j is Integer )

assume A10: j in dom f1 ; :: thesis: f1 . j is Integer

F . j = f1 . j by A6, A10, FINSEQ_1:def 7;

hence f1 . j is Integer by A5, A10, A9; :: thesis: verum

Sum F = (Sum f1) + m by A6, FVSUM_1:71;

then Sum F = i1 + i2 ;

hence Sum F is Integer ; :: thesis: verum

proof

A13:
for k being Nat holds S
let F be FinSequence of F_Complex; :: thesis: ( len F = 0 & ( for i being Element of NAT st i in dom F holds

F . i is Integer ) implies Sum F is Integer )

assume that

A12: len F = 0 and

for i being Element of NAT st i in dom F holds

F . i is Integer ; :: thesis: Sum F is Integer

( 0 -tuples_on the carrier of F_Complex = {{}} & F = {} ) by A12, COMPUT_1:5;

then F is Element of 0 -tuples_on the carrier of F_Complex by TARSKI:def 1;

hence Sum F is Integer by COMPLFLD:7, FVSUM_1:74; :: thesis: verum

end;F . i is Integer ) implies Sum F is Integer )

assume that

A12: len F = 0 and

for i being Element of NAT st i in dom F holds

F . i is Integer ; :: thesis: Sum F is Integer

( 0 -tuples_on the carrier of F_Complex = {{}} & F = {} ) by A12, COMPUT_1:5;

then F is Element of 0 -tuples_on the carrier of F_Complex by TARSKI:def 1;

hence Sum F is Integer by COMPLFLD:7, FVSUM_1:74; :: thesis: verum

len G = len G ;

hence Sum G is Integer by A1, A13; :: thesis: verum