for X being RealUnitarySpace
for f being linear-Functional of X
for y1, y2 being Point of X st ( for x being Point of X holds
( f . x = x .|. y1 & f . x = x .|. y2 ) ) holds
y1 = y2