let c be XFinSequence of REAL ; :: thesis: ( len c = 0 implies for x being Nat holds (seq_p c) . x = 0 )

assume AS: len c = 0 ; :: thesis: for x being Nat holds (seq_p c) . x = 0

let x be Nat; :: thesis: (seq_p c) . x = 0

L1: (seq_p c) . x = Sum (c (#) (seq_a^ (x,1,0))) by defseqp;

reconsider f = c (#) (seq_a^ (x,1,0)) as Sequence ;

dom f = (dom c) /\ (dom (seq_a^ (x,1,0))) by VALUED_1:def 4;

then L2: f = {} by AS;

reconsider f = f as XFinSequence of REAL ;

thus (seq_p c) . x = 0 by L2, L1; :: thesis: verum

assume AS: len c = 0 ; :: thesis: for x being Nat holds (seq_p c) . x = 0

let x be Nat; :: thesis: (seq_p c) . x = 0

L1: (seq_p c) . x = Sum (c (#) (seq_a^ (x,1,0))) by defseqp;

reconsider f = c (#) (seq_a^ (x,1,0)) as Sequence ;

dom f = (dom c) /\ (dom (seq_a^ (x,1,0))) by VALUED_1:def 4;

then L2: f = {} by AS;

reconsider f = f as XFinSequence of REAL ;

thus (seq_p c) . x = 0 by L2, L1; :: thesis: verum