let x be real-valued FinSequence; :: thesis: |(x,(0* (len x)))| = 0

set n = len x;

x is FinSequence of REAL by Lm1;

then reconsider p1 = x as Element of (len x) -tuples_on REAL by FINSEQ_2:92;

A1: 0* (len x) = (len x) |-> 0 by EUCLID:def 4;

|(x,(0* (len x)))| = Sum (mlt (p1,(0* (len x))))

.= Sum (0* (len x)) by Th2

.= 0 by A1, RVSUM_1:81 ;

hence |(x,(0* (len x)))| = 0 ; :: thesis: verum

set n = len x;

x is FinSequence of REAL by Lm1;

then reconsider p1 = x as Element of (len x) -tuples_on REAL by FINSEQ_2:92;

A1: 0* (len x) = (len x) |-> 0 by EUCLID:def 4;

|(x,(0* (len x)))| = Sum (mlt (p1,(0* (len x))))

.= Sum (0* (len x)) by Th2

.= 0 by A1, RVSUM_1:81 ;

hence |(x,(0* (len x)))| = 0 ; :: thesis: verum