let r be Real; :: thesis: |.r.| = (max+ r) + (max- r)

now :: thesis: ( ( 0 <= r & |.r.| = (max+ r) + (max- r) ) or ( r < 0 & |.r.| = (max+ r) + (max- r) ) )

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

case A1: 0 <= r ; :: thesis: |.r.| = (max+ r) + (max- r)

then ( max+ r = r & max- r = 0 ) by XXREAL_0:def 10;
hence |.r.| = (max+ r) + (max- r) by A1, ABSVALUE:def 1; :: thesis: verum

end;

case A2: r < 0 ; :: thesis: |.r.| = (max+ r) + (max- r)

then ( max+ r = 0 & max- r = - r ) by XXREAL_0:def 10;
hence |.r.| = (max+ r) + (max- r) by A2, ABSVALUE:def 1; :: thesis: verum

end;

end;

end;

hence |.r.| = (max+ r) + (max- r) ; :: thesis: verum