let a be Nat; :: thesis: for ft being FinSequence of REAL st a in dom ft holds
(Sum (Del (ft,a))) + (ft . a) = Sum ft
let ft be FinSequence of REAL ; :: thesis: ( a in dom ft implies (Sum (Del (ft,a))) + (ft . a) = Sum ft )
defpred S₁[ Nat] means ( $1 in dom ft implies (ft . $1) + (Sum (Del (ft,$1))) = Sum ft );
A1: for a being Nat st S₁[a] holds
S₁[a + 1]

proof

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

now :: thesis: S₁[a + 1]

per cases ( a = 0 or ( a > 0 & a < len ft ) or a >= len ft ) ;

suppose A2: a = 0 ; :: thesis: S₁[a + 1]

thus S₁[a + 1] :: thesis: verum

proof

reconsider ft1 = ft . 1 as Element of REAL by XREAL_0:def 1;
assume a + 1 in dom ft ; :: thesis: (ft . (a + 1)) + (Sum (Del (ft,(a + 1)))) = Sum ft
then a + 1 <= len ft by FINSEQ_3:25;
then <*(ft . 1)*> ^ (Del (ft,1)) = ft by A2, Lm15;
then Sum ft = (Sum <*ft1*>) + (Sum (Del (ft,1))) by RVSUM_1:75
.= (ft . 1) + (Sum (Del (ft,1))) by FINSOP_1:11 ;
hence (ft . (a + 1)) + (Sum (Del (ft,(a + 1)))) = Sum ft by A2; :: thesis: verum

end;

end;

suppose ( a > 0 & a < len ft ) ; :: thesis: S₁[a + 1]

then ( a + 1 >= 1 & a + 1 <= len ft ) by NAT_1:11, NAT_1:13;
then A3: a + 1 in dom ft by FINSEQ_3:25;
then consider fs1, fs2 being FinSequence such that
A4: ft = (fs1 ^ <*(ft . (a + 1))*>) ^ fs2 and
A5: len fs1 = (a + 1) - 1 and
len fs2 = (len ft) - (a + 1) by Lm10;
reconsider fta1 = ft . (a + 1) as Element of REAL by XREAL_0:def 1;
A6: Del (ft,(a + 1)) = fs1 ^ fs2 by A3, A4, A5, Lm11;
reconsider fs2 = fs2 as FinSequence of REAL by A4, FINSEQ_1:36;
reconsider fs1 = fs1 as FinSequence of REAL by A6, FINSEQ_1:36;
Sum ft = (Sum (fs1 ^ <*(ft . (a + 1))*>)) + (Sum fs2) by A4, RVSUM_1:75
.= ((Sum fs1) + (Sum <*fta1*>)) + (Sum fs2) by RVSUM_1:75
.= (fta1 + (Sum fs1)) + (Sum fs2) by FINSOP_1:11
.= (ft . (a + 1)) + ((Sum fs1) + (Sum fs2)) ;
hence S₁[a + 1] by A6, RVSUM_1:75; :: thesis: verum

end;

suppose a >= len ft ; :: thesis: S₁[a + 1]

then a + 1 > len ft by NAT_1:13;
hence S₁[a + 1] by FINSEQ_3:25; :: thesis: verum

end;

end;

end;

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

end;

A7: S₁[ 0 ] by FINSEQ_3:25;
for a being Nat holds S₁[a] from NAT_1:sch 2(A7, A1);
hence ( a in dom ft implies (Sum (Del (ft,a))) + (ft . a) = Sum ft ) ; :: thesis: verum