let i be Nat; :: thesis: for r being Element of F_Real holds Sum (i |-> r) = i * r
let r be Element of F_Real; :: thesis: Sum (i |-> r) = i * r
defpred S₁[ Nat] means Sum ($1 |-> r) = $1 * r;
A1: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A2: Sum (i |-> r) = i * r ; :: thesis: S₁[i + 1]
thus Sum ((i + 1) |-> r) = Sum ((i |-> r) ^ <*r*>) by FINSEQ_2:60
.= (i * r) + r by A2, FVSUM_1:71
.= (i * r) + (1 * r) by BINOM:13
.= (i + 1) * r by BINOM:15 ; :: thesis: verum

end;

0 |-> r = <*> the carrier of F_Real ;
then Sum (0 |-> r) = 0. F_Real by RLVECT_1:43
.= 0 * r by BINOM:12 ;
then A3: S₁[ 0 ] ;
for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A1);
hence Sum (i |-> r) = i * r ; :: thesis: verum