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;
P0: S₁[ 0 ] ;

P1: now

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

now

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 AS: ( 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:6;
then Q2: n + 1 in dom f by FINSEQ_1:def 3, AS;
P11: len g = n by AS, NAT_1:11, FINSEQ_1:80;
f = (f | n) ^ <*(f . (n + 1))*> by AS, FINSEQ_3:61
.= g ^ <*(f /. (n + 1))*> by Q2, PARTFUN1:def 8 ;
then P12: Sum f = (Sum g) + (Sum <*(f /. (n + 1))*>) by RLVECT_1:58;
A0: dom ({i} --> v) = {i} by FUNCOP_1:19;
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 A1: 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 A2: f2 = {i} --> v ; :: thesis: Sum b₁ = v

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

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

then dom f2 = {(n + 1)} by A2, FUNCOP_1:19;
then g = f1 | (Seg n) by AS, A1, A2, FINSEQ_3:15, FUNCT_4:76
.= ((Seg (len f)) /\ (Seg n)) --> (0. RS) by A1, FUNCOP_1:18 ;
then P13: g = (Seg n) --> (0. RS) by AS, NAT_1:11, FINSEQ_1:9;
A5: n + 1 in {(n + 1)} by ZFMISC_1:37;
then n + 1 in dom f2 by A2, A3, FUNCOP_1:19;
then f . (n + 1) = f2 . (n + 1) by AS, A2, FUNCT_4:14
.= v by A2, A3, A5, FUNCOP_1:13 ;
then P14: f /. (n + 1) = v by Q2, PARTFUN1:def 8;
Sum g = 0. RS by P11, P13, SLM0010;
hence Sum f = (0. RS) + v by P12, P14, RLVECT_1:61
.= v by RLVECT_1:10 ;
:: thesis: verum

end;

suppose A6: 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 AS, FINSEQ_1:3, NAT_1:13;
then P16: i in Seg (len g) by P11, FINSEQ_1:3;
g = (f1 | (Seg n)) +* (f2 | (Seg n)) by AS, A1, A2, FUNCT_4:75
.= (((Seg (len f)) /\ (Seg n)) --> (0. RS)) +* (f2 | (Seg n)) by A1, FUNCOP_1:18
.= ((Seg (len g)) --> (0. RS)) +* (f2 | (Seg n)) by AS, P11, NAT_1:11, FINSEQ_1:9
.= ((Seg (len g)) --> (0. RS)) +* (({i} /\ (Seg n)) --> v) by A2, FUNCOP_1:18 ;
then P17: g = ((Seg (len g)) --> (0. RS)) +* ({i} --> v) by P11, P16, ZFMISC_1:52;
not {(n + 1)} c= dom f2 by A0, A2, A6, ZFMISC_1:6;
then not n + 1 in dom f2 by ZFMISC_1:37;
then f . (n + 1) = f1 . (n + 1) by AS, A1, A2, FUNCT_4:12
.= 0. RS by AS, A1, FINSEQ_1:6, FUNCOP_1:13 ;
then P18: f /. (n + 1) = 0. RS by Q2, PARTFUN1:def 8;
Sum g = v by P16, P17, P11, P10;
hence Sum f = v + (0. RS) by P12, P18, RLVECT_1:61
.= v by RLVECT_1:10 ;
:: thesis: verum

end;

end;

end;

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

end;

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