theorem Th30: :: EUCLID_7:31

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