theorem Th2: :: HILBERT2:2

for x, y being set
for f, g being FinSequence st <*x*> ^ f = <*y*> ^ g holds
f = g