defpred S₁[ Nat] means for p being FinSequence of REAL
for i being Nat
for r being Real st len p = $1 & i in dom p & p . i = r & ( for k being Nat st k in dom p & k <> i holds
p . k = 0 ) holds
Sum p = r;
A1: S₁[ 0 ]

proof

let p be FinSequence of REAL ; :: thesis: for i being Nat
for r being Real st len p = 0 & i in dom p & p . i = r & ( for k being Nat st k in dom p & k <> i holds
p . k = 0 ) holds
Sum p = r
let i be Nat; :: thesis: for r being Real st len p = 0 & i in dom p & p . i = r & ( for k being Nat st k in dom p & k <> i holds
p . k = 0 ) holds
Sum p = r
let r be Real; :: thesis: ( len p = 0 & i in dom p & p . i = r & ( for k being Nat st k in dom p & k <> i holds
p . k = 0 ) implies Sum p = r )
assume that
A2: len p = 0 and
A3: i in dom p and
p . i = r and
for k being Nat st k in dom p & k <> i holds
p . k = 0 ; :: thesis: Sum p = r
p = <*> REAL by A2;
hence Sum p = r by A3; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
S₁[n + 1]

proof

let p be FinSequence of REAL ; :: thesis: for i being Nat
for r being Real st len p = n + 1 & i in dom p & p . i = r & ( for k being Nat st k in dom p & k <> i holds
p . k = 0 ) holds
Sum p = r
let i be Nat; :: thesis: for r being Real st len p = n + 1 & i in dom p & p . i = r & ( for k being Nat st k in dom p & k <> i holds
p . k = 0 ) holds
Sum p = r
let r be Real; :: thesis: ( len p = n + 1 & i in dom p & p . i = r & ( for k being Nat st k in dom p & k <> i holds
p . k = 0 ) implies Sum p = r )
assume that
A6: len p = n + 1 and
A7: i in dom p and
A8: p . i = r and
A9: for k being Nat st k in dom p & k <> i holds
p . k = 0 ; :: thesis: Sum p = r
consider q being FinSequence of REAL , a being Element of REAL such that
A10: p = q ^ <*a*> by A6, FINSEQ_2:19;
A11: len p = (len q) + 1 by A10, FINSEQ_2:16;
A12: ( 1 <= i & i <= n + 1 ) by A6, A7, FINSEQ_3:25;

per cases ( i <> n + 1 or i = n + 1 ) ;

suppose A13: i <> n + 1 ; :: thesis: Sum p = r

then ( 1 <= i & i < n + 1 ) by A12, XXREAL_0:1;
then A14: ( 1 <= i & i <= n ) by INT_1:7;
A15: q . i = r

proof

q = p | (dom q) by A10, FINSEQ_1:21;
hence q . i = r by A6, A8, A11, A14, FUNCT_1:47, FINSEQ_3:25; :: thesis: verum

end;

A17: for k being Nat st k in dom q & k <> i holds
q . k = 0

proof

let k be Nat; :: thesis: ( k in dom q & k <> i implies q . k = 0 )
assume that
A18: k in dom q and
A19: k <> i ; :: thesis: q . k = 0
A20: dom q c= dom p by A10, FINSEQ_1:26;
q . k = p . k by A10, A18, FINSEQ_1:def 7
.= 0 by A9, A18, A19, A20 ;
hence q . k = 0 ; :: thesis: verum

end;

A21: ( 1 <= n + 1 & n + 1 <= n + 1 ) by XREAL_1:31;
a = p . (n + 1) by A6, A10, A11, FINSEQ_1:42
.= 0 by A6, A9, A13, A21, FINSEQ_3:25 ;
then Sum p = (Sum q) + 0 by A10, RVSUM_1:74
.= r by A5, A6, A11, A14, A15, A17, FINSEQ_3:25 ;
hence Sum p = r ; :: thesis: verum

end;

suppose A22: i = n + 1 ; :: thesis: Sum p = r

for k being object st k in dom q holds
q . k = 0

proof

let k be object ; :: thesis: ( k in dom q implies q . k = 0 )
assume A23: k in dom q ; :: thesis: q . k = 0
then reconsider k = k as Nat ;
A24: ( 1 <= k & k <= n ) by A6, A11, A23, FINSEQ_3:25;
A25: dom q c= dom p by A10, FINSEQ_1:26;
A26: k + 0 < n + 1 by A24, XREAL_1:8;
q . k = p . k by A10, A23, FINSEQ_1:def 7
.= 0 by A9, A22, A23, A25, A26 ;
hence q . k = 0 ; :: thesis: verum

end;

then A27: q = n |-> 0 by A6, A11, Th5;
A28: a = r by A6, A8, A10, A11, A22, FINSEQ_1:42;
Sum p = (Sum q) + a by A10, RVSUM_1:74
.= 0 + r by A27, A28, RVSUM_1:81 ;
hence Sum p = r ; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A29: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A4);
let p be FinSequence of REAL ; :: thesis: for i being Nat
for r being Real st i in dom p & p . i = r & ( for k being Nat st k in dom p & k <> i holds
p . k = 0 ) holds
Sum p = r
let i be Nat; :: thesis: for r being Real st i in dom p & p . i = r & ( for k being Nat st k in dom p & k <> i holds
p . k = 0 ) holds
Sum p = r
let r be Real; :: thesis: ( i in dom p & p . i = r & ( for k being Nat st k in dom p & k <> i holds
p . k = 0 ) implies Sum p = r )
assume A30: ( i in dom p & p . i = r & ( for k being Nat st k in dom p & k <> i holds
p . k = 0 ) ) ; :: thesis: Sum p = r
len p is Nat ;
hence Sum p = r by A29, A30; :: thesis: verum