let a be Element of INT.Ring; :: thesis: absint . a = |.a.|
reconsider a9 = a as Integer ;
absint . a = absreal . a9 by Def5
.= |.a9.| by EUCLID:def 2 ;
hence absint . a = |.a.| ; :: thesis: verum