let n be Nat; :: thesis: for c being Complex holds Sum (n --> c) = n * c
let c be Complex; :: thesis: Sum (n --> c) = n * c
set Fn = n --> c;
reconsider Fn = n --> c as XFinSequence of COMPLEX by Lm2;
A1: dom Fn = n by FUNCOP_1:13;
now :: thesis: Sum (n --> c) = n * c
per cases ( dom Fn = 0 or dom Fn > 0 ) ;
suppose dom Fn = 0 ; :: thesis: Sum (n --> c) = n * c
hence Sum (n --> c) = n * c by A1; :: thesis: verum
end;
suppose A2: dom Fn > 0 ; :: thesis: Sum (n --> c) = n * c
then consider f being sequence of COMPLEX such that
A3: f . 0 = Fn . 0 and
A4: for k being Nat st k + 1 < len Fn holds
f . (k + 1) = addcomplex . ((f . k),(Fn . (k + 1))) and
A5: Sum Fn = f . ((len Fn) - 1) by Def8;
defpred S1[ Nat] means ( $1 < len Fn implies f . $1 = ($1 + 1) * c );
A6: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A7: S1[m] ; :: thesis: S1[m + 1]
assume A8: m + 1 < len Fn ; :: thesis: f . (m + 1) = ((m + 1) + 1) * c
then f . (m + 1) = addcomplex . ((f . m),(Fn . (m + 1))) by A4;
then A9: f . (m + 1) = (f . m) + (Fn . (m + 1)) by BINOP_2:def 3;
Fn . (m + 1) = c by A1, FUNCOP_1:7, A8, AFINSQ_1:86;
hence f . (m + 1) = ((m + 1) + 1) * c by A7, A8, A9, NAT_1:13; :: thesis: verum
end;
reconsider lenFn1 = (len Fn) - 1 as Element of NAT by A2, NAT_1:20;
A10: lenFn1 < lenFn1 + 1 by NAT_1:13;
A11: S1[ 0 ] by A3, A1, FUNCOP_1:7, AFINSQ_1:86;
for m being Nat holds S1[m] from NAT_1:sch 2(A11, A6);
hence Sum (n --> c) = n * c by A5, A10, A1; :: thesis: verum
end;
end;
end;
hence Sum (n --> c) = n * c ; :: thesis: verum