let RS be RealLinearSpace; :: thesis: for f being FinSequence of RS
for v being Element of RS
for i being Nat st i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) holds
Sum f = v
let f be FinSequence of RS; :: thesis: for v being Element of RS
for i being Nat st i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) holds
Sum f = v
let v be Element of RS; :: thesis: for i being Nat st i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) holds
Sum f = v
let i be Nat; :: thesis: ( i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) implies Sum f = v )
defpred S₁[ Nat] means for g being FinSequence of RS st len g = $1 & i in Seg (len g) & g = ((Seg (len g)) --> (0. RS)) +* ({i} --> v) holds
Sum g = v;
A1: S₁[ 0 ] ;

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

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

now :: thesis: for f being FinSequence of RS st len f = n + 1 & i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) holds
for f1 being Function st f1 = (Seg (len f)) --> (0. RS) holds
for f2 being Function st f2 = {i} --> v holds
Sum f = v

let f be FinSequence of RS; :: thesis: ( len f = n + 1 & i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) implies for f1 being Function st f1 = (Seg (len f)) --> (0. RS) holds
for f2 being Function st f2 = {i} --> v holds
Sum b₃ = v )
assume A4: ( len f = n + 1 & i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) ) ; :: thesis: for f1 being Function st f1 = (Seg (len f)) --> (0. RS) holds
for f2 being Function st f2 = {i} --> v holds
Sum b₃ = v
reconsider g = f | n as FinSequence of RS ;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A5: n + 1 in dom f by A4, FINSEQ_1:def 3;
A6: len g = n by A4, FINSEQ_1:59, NAT_1:11;
f = (f | n) ^ <*(f . (n + 1))*> by A4, FINSEQ_3:55
.= g ^ <*(f /. (n + 1))*> by A5, PARTFUN1:def 6 ;
then A7: Sum f = (Sum g) + (Sum <*(f /. (n + 1))*>) by RLVECT_1:41;
A8: dom ({i} --> v) = {i} by FUNCOP_1:13;
let f1 be Function; :: thesis: ( f1 = (Seg (len f)) --> (0. RS) implies for f2 being Function st f2 = {i} --> v holds
Sum b₂ = v )
assume A9: f1 = (Seg (len f)) --> (0. RS) ; :: thesis: for f2 being Function st f2 = {i} --> v holds
Sum b₂ = v
let f2 be Function; :: thesis: ( f2 = {i} --> v implies Sum b₁ = v )
assume A10: f2 = {i} --> v ; :: thesis: Sum b₁ = v

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

suppose A11: i = n + 1 ; :: thesis: Sum b₁ = v

then dom f2 = {(n + 1)} by A10, FUNCOP_1:13;
then g = f1 | (Seg n) by A4, A9, A10, FINSEQ_3:14, FUNCT_4:72
.= ((Seg (len f)) /\ (Seg n)) --> (0. RS) by A9, FUNCOP_1:12 ;
then A12: g = (Seg n) --> (0. RS) by A4, FINSEQ_1:7, NAT_1:11;
A13: n + 1 in {(n + 1)} by ZFMISC_1:31;
then n + 1 in dom f2 by A10, A11, FUNCOP_1:13;
then f . (n + 1) = f2 . (n + 1) by A4, A10, FUNCT_4:13
.= v by A10, A11, A13, FUNCOP_1:7 ;
then A14: f /. (n + 1) = v by A5, PARTFUN1:def 6;
Sum g = 0. RS by A6, A12, Th28;
hence Sum f = (0. RS) + v by A7, A14, RLVECT_1:44
.= v by RLVECT_1:4 ;
:: thesis: verum

end;

suppose A15: i <> n + 1 ; :: thesis: Sum b₁ = v

then ( i < n + 1 or i > n + 1 ) by XXREAL_0:1;
then ( 1 <= i & i <= n ) by A4, FINSEQ_1:1, NAT_1:13;
then A16: i in Seg (len g) by A6;
g = (f1 | (Seg n)) +* (f2 | (Seg n)) by A4, A9, A10, FUNCT_4:71
.= (((Seg (len f)) /\ (Seg n)) --> (0. RS)) +* (f2 | (Seg n)) by A9, FUNCOP_1:12
.= ((Seg (len g)) --> (0. RS)) +* (f2 | (Seg n)) by A4, A6, FINSEQ_1:7, NAT_1:11
.= ((Seg (len g)) --> (0. RS)) +* (({i} /\ (Seg n)) --> v) by A10, FUNCOP_1:12 ;
then A17: g = ((Seg (len g)) --> (0. RS)) +* ({i} --> v) by A6, A16, ZFMISC_1:46;
not {(n + 1)} c= dom f2 by A8, A10, A15, ZFMISC_1:3;
then not n + 1 in dom f2 by ZFMISC_1:31;
then f . (n + 1) = f1 . (n + 1) by A4, A9, A10, FUNCT_4:11
.= 0. RS by A4, A9, FINSEQ_1:4, FUNCOP_1:7 ;
then A18: f /. (n + 1) = 0. RS by A5, PARTFUN1:def 6;
Sum g = v by A16, A17, A6, A3;
hence Sum f = v + (0. RS) by A7, A18, RLVECT_1:44
.= v by RLVECT_1:4 ;
:: thesis: verum

end;

end;

end;

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

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence ( i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) implies Sum f = v ) ; :: thesis: verum