let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds
( |(p,p)| = 0 iff |.p.| = 0 )
let p be Point of (TOP-REAL n); :: thesis: ( |(p,p)| = 0 iff |.p.| = 0 )
A1: ( |(p,p)| = 0 ^2 implies |.p.| = 0 )

proof

assume |(p,p)| = 0 ^2 ; :: thesis: |.p.| = 0
then |.p.| ^2 = 0 by Th34;
hence |.p.| = 0 by XCMPLX_1:6; :: thesis: verum

end;

( |.p.| = 0 implies |(p,p)| = 0 ^2 ) by Th34;
hence ( |(p,p)| = 0 iff |.p.| = 0 ) by A1; :: thesis: verum