let x be ExtReal; :: thesis: for a being Real st x = a holds

|.x.| = |.a.|

let a be Real; :: thesis: ( x = a implies |.x.| = |.a.| )

assume A1: x = a ; :: thesis: |.x.| = |.a.|

reconsider x = x as R_eal by XXREAL_0:def 1;

|.x.| = |.a.|

let a be Real; :: thesis: ( x = a implies |.x.| = |.a.| )

assume A1: x = a ; :: thesis: |.x.| = |.a.|

reconsider x = x as R_eal by XXREAL_0:def 1;