theorem :: PRGCOR_2:9

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