let r be Real; :: thesis: |.r.| = |.(R_EAL r).|

per cases ( 0 <= r or r < 0 ) ;

suppose A1: 0 <= r ; :: thesis: |.r.| = |.(R_EAL r).|

then |.(R_EAL r).| = R_EAL r by EXTREAL1:def 1;
hence |.r.| = |.(R_EAL r).| by A1, ABSVALUE:def 1; :: thesis: verum

end;

suppose A2: r < 0 ; :: thesis: |.r.| = |.(R_EAL r).|

then |.(R_EAL r).| = - (R_EAL r) by EXTREAL1:def 1;
then |.(R_EAL r).| = R_EAL (- r) by SUPINF_2:2;
hence |.r.| = |.(R_EAL r).| by A2, ABSVALUE:def 1; :: thesis: verum

end;

end;