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 )

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

( |(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

( |.p.| = 0 implies |(p,p)| = 0 ^2 )
by Th34;
assume
|(p,p)| = 0 ^2
; :: thesis: |.p.| = 0

then |.p.| ^2 = 0 by Th34;

hence |.p.| = 0 by XCMPLX_1:6; :: thesis: verum

end;then |.p.| ^2 = 0 by Th34;

hence |.p.| = 0 by XCMPLX_1:6; :: thesis: verum

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