:: deftheorem defines vector_add_prg PRGCOR_2:def 6 :
for a, b, c being XFinSequence of REAL
for m being Integer holds
( m vector_add_prg c,a,b iff ( len c = m & len a = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = (a . i) + (b . i) ) ) ) );