:: deftheorem defines vector_minus_prg PRGCOR_2:def 5 :
for b, c being XFinSequence of REAL
for m being Integer holds
( m vector_minus_prg c,b iff ( len c = 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 = - (b . i) ) ) ) );