for n being Nat
for x0 being Element of REAL n holds x0 = Sum (ProjFinSeq x0)