for b being non empty XFinSequence of REAL
for m being Nat st b . 0 is Nat & len b = m & b . 0 < m holds
( ex c being XFinSequence of REAL st m vector_minus_prg c,b & ( for c being non empty XFinSequence of REAL st m vector_minus_prg c,b holds
XFS2FS* c = - (XFS2FS* b) ) )