let u be Element of (TOP-REAL 3); :: thesis: ( u is zero iff |(u,u)| = 0 )
reconsider un = u as Element of REAL 3 by EUCLID:22;
hereby :: thesis: ( |(u,u)| = 0 implies u is zero )
assume u is zero ; :: thesis: |(u,u)| = 0
then 0.REAL 3 = u by EUCLID:66;
then |(un,un)| = 0 by EUCLID_4:17;
hence |(u,u)| = 0 ; :: thesis: verum
end;
assume |(u,u)| = 0 ; :: thesis: u is zero
then un = 0.REAL 3 by EUCLID_4:17;
hence u is zero by EUCLID:66; :: thesis: verum