let a be Real; :: thesis: |[a]| /. 1 = a
reconsider y = a as Element of REAL by XREAL_0:def 1;
thus |[a]| /. 1 = <*y*> /. 1
.= a by FINSEQ_4:16 ; :: thesis: verum