:: deftheorem defines vector_sub_prg PRGCOR_2:def 7 :
for a, b, c being XFinSequence of REAL
for m being Integer holds
( m vector_sub_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) ) ) ) );