let X be RealNormSpace; :: thesis: for x being Point of X st ( for e being Real st e > 0 holds

||.x.|| < e ) holds

x = 0. X

let x be Point of X; :: thesis: ( ( for e being Real st e > 0 holds

||.x.|| < e ) implies x = 0. X )

assume A1: for e being Real st e > 0 holds

||.x.|| < e ; :: thesis: x = 0. X

||.x.|| < e ) holds

x = 0. X

let x be Point of X; :: thesis: ( ( for e being Real st e > 0 holds

||.x.|| < e ) implies x = 0. X )

assume A1: for e being Real st e > 0 holds

||.x.|| < e ; :: thesis: x = 0. X

now :: thesis: not x <> 0. X

hence
x = 0. X
; :: thesis: verumassume
x <> 0. X
; :: thesis: contradiction

then 0 <> ||.x.|| by NORMSP_0:def 5;

then 0 < ||.x.|| ;

hence contradiction by A1; :: thesis: verum

end;then 0 <> ||.x.|| by NORMSP_0:def 5;

then 0 < ||.x.|| ;

hence contradiction by A1; :: thesis: verum