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