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

per cases ( 0 <= x or 0 > x ) ;

suppose A2: 0 <= x ; :: thesis: |.x.| = |.a.|

hence |.x.| = a by A1, Def1
.= |.a.| by A2, A1, ABSVALUE:def 1 ;
:: thesis: verum

end;

suppose A3: 0 > x ; :: thesis: |.x.| = |.a.|

hence |.x.| = - x by Def1
.= |.a.| by A3, A1, ABSVALUE:def 1 ;
:: thesis: verum

end;

end;