let X be RealUnitarySpace; :: thesis: for x being Point of X holds ||.x.|| ^2 = x .|. x
let x be Point of X; :: thesis: ||.x.|| ^2 = x .|. x
0 <= x .|. x by BHSP_1:def 2;
hence ||.x.|| ^2 = x .|. x by SQUARE_1:def 2; :: thesis: verum