theorem :: PRGCOR_2:8

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_add_prg c,a,b & ( for c being non empty XFinSequence of REAL st m vector_add_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) )