defpred S₁[ Nat] means for f being FinSequence of REAL
for m being Real st len f = $1 holds
Sum (($1 |-> m) - f) = ($1 * m) - (Sum f);
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

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

proof

let f be FinSequence of REAL ; :: thesis: for m being Real st len f = n + 1 holds
Sum (((n + 1) |-> m) - f) = ((n + 1) * m) - (Sum f)
let m be Real; :: thesis: ( len f = n + 1 implies Sum (((n + 1) |-> m) - f) = ((n + 1) * m) - (Sum f) )
A3: len <*m*> = 1 by FINSEQ_1:39;
assume A4: len f = n + 1 ; :: thesis: Sum (((n + 1) |-> m) - f) = ((n + 1) * m) - (Sum f)
then f <> {} ;
then consider f1 being FinSequence of REAL , x being Element of REAL such that
A5: f = f1 ^ <*x*> by HILBERT2:4;
reconsider mm = m as Element of REAL by XREAL_0:def 1;
A6: n + 1 = (len f1) + 1 by A4, A5, FINSEQ_2:16;
then A7: len (n |-> m) = len f1 by CARD_1:def 7;
A8: len <*x*> = 1 by FINSEQ_1:39;
((n + 1) |-> m) - f = ((n |-> m) ^ <*m*>) - (f1 ^ <*x*>) by A5, FINSEQ_2:60
.= ((n |-> mm) - f1) ^ (<*mm*> - <*x*>) by A7, A8, A3, Th46
.= ((n |-> m) - f1) ^ <*(m - x)*> by RVSUM_1:29 ;
hence Sum (((n + 1) |-> m) - f) = (Sum ((n |-> m) - f1)) + (m - x) by RVSUM_1:74
.= ((n * m) - (Sum f1)) + (m - x) by A2, A6
.= ((n + 1) * m) - ((Sum f1) + x)
.= ((n + 1) * m) - (Sum f) by A5, RVSUM_1:74 ;
:: thesis: verum

end;

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

end;

A9: S₁[ 0 ]

proof

let f be FinSequence of REAL ; :: thesis: for m being Real st len f = 0 holds
Sum ((0 |-> m) - f) = (0 * m) - (Sum f)
let m be Real; :: thesis: ( len f = 0 implies Sum ((0 |-> m) - f) = (0 * m) - (Sum f) )
assume len f = 0 ; :: thesis: Sum ((0 |-> m) - f) = (0 * m) - (Sum f)
then Sum f = 0 by PROB_3:62;
hence Sum ((0 |-> m) - f) = (0 * m) - (Sum f) by RVSUM_1:28, RVSUM_1:72; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A9, A1);
hence for f being FinSequence of REAL
for m being Real holds Sum (((len f) |-> m) - f) = ((len f) * m) - (Sum f) ; :: thesis: verum