defpred S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
S1[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 ;
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
.= ((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 ;
:: thesis: verum
end;
hence S1[n + 1] ; :: thesis: verum
end;
A9: S1[ 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 ; :: thesis: verum
end;
for n being Nat holds S1[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