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
now :: thesis: for x being Point of X holds x .|. (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;
then (y1 - y2) .|. (y1 - y2) = 0 ;
then y1 - y2 = 0. X by BHSP_1:def 2;
hence y1 = y2 by RLVECT_1:21; :: thesis: verum