let k be Nat; :: thesis: for seq being Complex_Sequence holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k)
let seq be Complex_Sequence; :: thesis: (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k)
defpred S₁[ Nat] means (Partial_Sums seq) . $1 = ((Partial_Sums (Shift seq)) . $1) + (seq . $1);
(Partial_Sums seq) . 0 = 0c + (seq . 0) by SERIES_1:def 1
.= ((Shift seq) . 0) + (seq . 0) by Def8
.= ((Partial_Sums (Shift seq)) . 0) + (seq . 0) by SERIES_1:def 1 ;
then A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) ; :: thesis: S₁[k + 1]
thus (Partial_Sums seq) . (k + 1) = (((Partial_Sums (Shift seq)) . k) + (seq . k)) + (seq . (k + 1)) by A3, SERIES_1:def 1
.= (((Partial_Sums (Shift seq)) . k) + ((Shift seq) . (k + 1))) + (seq . (k + 1)) by Def8
.= ((Partial_Sums (Shift seq)) . (k + 1)) + (seq . (k + 1)) by SERIES_1:def 1 ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) ; :: thesis: verum