theorem Th81: :: ANPROJ_8:100

for u being Element of (TOP-REAL 3)
for uf being FinSequence of F_Real st u = uf & <*uf*> @ = <*<*0*>,<*0*>,<*0*>*> holds
u = 0. (TOP-REAL 3)