let X be RealUnitarySpace; :: thesis: 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

let f be linear-Functional of X; :: thesis: 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

let y1, y2 be Point of X; :: thesis: ( ( for x being Point of X holds

( f . x = x .|. y1 & f . x = x .|. y2 ) ) implies y1 = y2 )

assume AS: for x being Point of X holds

( f . x = x .|. y1 & f . x = x .|. y2 ) ; :: thesis: y1 = y2

then y1 - y2 = 0. X by BHSP_1:def 2;

hence y1 = y2 by RLVECT_1:21; :: thesis: verum

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

let f be linear-Functional of X; :: thesis: 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

let y1, y2 be Point of X; :: thesis: ( ( for x being Point of X holds

( f . x = x .|. y1 & f . x = x .|. y2 ) ) implies y1 = y2 )

assume AS: for x being Point of X holds

( f . x = x .|. y1 & f . x = x .|. y2 ) ; :: thesis: y1 = y2

now :: thesis: for x being Point of X holds x .|. (y1 - y2) = 0

then
(y1 - y2) .|. (y1 - y2) = 0
;let x be Point of X; :: thesis: x .|. (y1 - y2) = 0

( f . x = x .|. y1 & f . x = x .|. y2 ) by AS;

then (x .|. y1) - (x .|. y2) = 0 ;

hence x .|. (y1 - y2) = 0 by BHSP_1:12; :: thesis: verum

end;( f . x = x .|. y1 & f . x = x .|. y2 ) by AS;

then (x .|. y1) - (x .|. y2) = 0 ;

hence x .|. (y1 - y2) = 0 by BHSP_1:12; :: thesis: verum

then y1 - y2 = 0. X by BHSP_1:def 2;

hence y1 = y2 by RLVECT_1:21; :: thesis: verum