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