let L be comRing; :: thesis: for I being Ideal of L
for F being FinSequence of L st ( for i being Nat st i in dom F holds
F . i in I ) holds
Sum F in I
let I be Ideal of L; :: thesis: for F being FinSequence of L st ( for i being Nat st i in dom F holds
F . i in I ) holds
Sum F in I
defpred S₁[ Nat] means for F being FinSequence of L st len F = $1 & ( for i being Nat st i in dom F holds
F . i in I ) holds
Sum F in I;
A1: S₁[ 0 ]

proof

let F be FinSequence of L; :: thesis: ( len F = 0 & ( for i being Nat st i in dom F holds
F . i in I ) implies Sum F in I )
assume ( len F = 0 & ( for i being Nat st i in dom F holds
F . i in I ) ) ; :: thesis: Sum F in I
then F = <*> the carrier of L ;
then Sum F = 0. L by RLVECT_1:43;
hence Sum F in I by IDEAL_1:2; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
let F be FinSequence of L; :: thesis: ( len F = n + 1 & ( for i being Nat st i in dom F holds
F . i in I ) implies Sum F in I )
assume A5: ( len F = n + 1 & ( for i being Nat st i in dom F holds
F . i in I ) ) ; :: thesis: Sum F in I
reconsider F0 = F | n as FinSequence of L ;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then n + 1 in dom F by A5, FINSEQ_1:def 3;
then reconsider af = F . (n + 1) as Element of I by A5;
A6: len F0 = n by FINSEQ_1:59, A5, NAT_1:11;
then A7: dom F0 = Seg n by FINSEQ_1:def 3;
A8: len F = (len F0) + 1 by A5, FINSEQ_1:59, NAT_1:11;
A9: F0 = F | (dom F0) by A6, FINSEQ_1:def 3;
A10: for i being Nat st i in dom F0 holds
F0 . i in I

proof

let i be Nat; :: thesis: ( i in dom F0 implies F0 . i in I )
assume A11: i in dom F0 ; :: thesis: F0 . i in I
dom F = Seg (n + 1) by A5, FINSEQ_1:def 3;
then dom F0 c= dom F by A7, FINSEQ_1:5, NAT_1:11;
then F . i in I by A5, A11;
hence F0 . i in I by A11, FUNCT_1:47; :: thesis: verum

end;

reconsider i1 = Sum F0 as Element of I by A6, A4, A10;
reconsider i2 = af as Element of I ;
Sum F = i1 + i2 by A5, A8, A9, RLVECT_1:38;
hence Sum F in I by IDEAL_1:def 1; :: thesis: verum

end;

A12: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
let F be FinSequence of L; :: thesis: ( ( for i being Nat st i in dom F holds
F . i in I ) implies Sum F in I )
assume A13: for i being Nat st i in dom F holds
F . i in I ; :: thesis: Sum F in I
len F is Nat ;
hence Sum F in I by A12, A13; :: thesis: verum