let r be R_eal; :: thesis: for i being Nat st r is real holds
Sum (i |-> r) = i * r
let i be Nat; :: thesis: ( r is real implies Sum (i |-> r) = i * r )
assume A0: r is real ; :: thesis: Sum (i |-> r) = i * r
defpred S1[ Nat] means Sum ($1 |-> r) = $1 * r;
A1: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A2: Sum (i |-> r) = i * r ; :: thesis: S1[i + 1]
reconsider i1 = i, One = 1 as ext-real number ;
thus Sum ((i + 1) |-> r) = Sum ((i |-> r) ^ <*r*>) by FINSEQ_2:60
.= (i * r) + r by A2, Th19
.= (i * r) + (1 * r) by XXREAL_3:81
.= (i1 + One) * r by A0, XXREAL_3:95
.= (i + 1) * r by XXREAL_3:def 2 ; :: thesis: verum
end;
A3: S1[ 0 ] by EXTREAL1:7, FINSEQ_2:58;
for i being Nat holds S1[i] from NAT_1:sch 2(A3, A1);
 hence Sum (i |-> r) = i * r ; :: thesis: verum