let r, s be Real; :: thesis: ( |.r.| + |.s.| = 0 implies r = 0 )
set aa = |.r.|;
set ab = |.s.|;
A1: ( 0 <= |.r.| & 0 <= |.s.| ) by COMPLEX1:46;
assume |.r.| + |.s.| = 0 ; :: thesis: r = 0
then |.r.| = 0 by A1;
hence r = 0 by ABSVALUE:2; :: thesis: verum