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: 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 A2: len f = 0 ; :: thesis: Sum ((0 |-> m) - f) = (0 * m) - (Sum f)
then A3: (len f) |-> m = <*> REAL by FINSEQ_2:72;
Sum f = 0 by A2, PROB_3:67;
hence Sum ((0 |-> m) - f) = (0 * m) - (Sum f) by A2, A3, RVSUM_1:49, RVSUM_1:102; :: thesis: verum

end;

A4: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: 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) )
assume A6: 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
A7: f = f1 ^ <*x*> by HILBERT2:4;
A8: n + 1 = (len f1) + 1 by A6, A7, FINSEQ_2:19;
then A9: ( len (n |-> m) = len f1 & len <*x*> = 1 & len <*m*> = 1 ) by FINSEQ_1:56, FINSEQ_1:def 18;
((n + 1) |-> m) - f = ((n |-> m) ^ <*m*>) - (f1 ^ <*x*>) by A7, FINSEQ_2:74
.= ((n |-> m) - f1) ^ (<*m*> - <*x*>) by A9, Th46
.= ((n |-> m) - f1) ^ <*(m - x)*> by RVSUM_1:50 ;
hence Sum (((n + 1) |-> m) - f) = (Sum ((n |-> m) - f1)) + (m - x) by RVSUM_1:104
.= ((n * m) - (Sum f1)) + (m - x) by A5, A8
.= ((n + 1) * m) - ((Sum f1) + x)
.= ((n + 1) * m) - (Sum f) by A7, RVSUM_1:104 ;
:: thesis: verum

end;

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

end;

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